A practical comparison of Alloy and Spin
Pamela Zave · Formal Aspects of Computing · 2014
Abstract 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.