caa a22 4500 605516375 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20150301xx s 000 0 eng 10.1007/s00165-014-0302-2 doi (NATIONALLICENCE)springer-10.1007/s00165-014-0302-2 Zave P. AT&T Laboratories-Research, Bedminster, NJ, USA aut A practical comparison of Alloy and Spin [Elektronische Daten] [P. Zave] Because potential users have to choose a formal method before they can start using one, research on assessing the applicability of specific formal methods might be as effective in encouraging their use as work on the methods themselves. This comparison of Alloy and Spin is based on a demanding project that exploited the full capabilities of both languages and tools. The study exposed issues not apparent from more superficial studies, and resulted in some unexpected conclusions. The paper provides tentative recommendations for two different classes of network protocol, a research agenda for solidifying the recommendations, and a few general lessons learned about research on selection of formal methods. British Computer Society, 2014 Lightweight modeling and analysis nationallicence Protocol verification nationallicence Distributed hash table nationallicence Chord nationallicence Formal Aspects of Computing Springer London 27/2(2015-03-01), 239-253 0934-5043 27:2<239 2015 27 165 https://doi.org/10.1007/s00165-014-0302-2 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0302-2 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Zave P. AT&T Laboratories-Research, Bedminster, NJ, USA aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/2(2015-03-01), 239-253 0934-5043 27:2<239 2015 27 165