An automated tool for analyzing Petri nets using Spin

The Spin model checker is a system that has been used to model and analyze a large number of applications in several domains including the aerospace industry. One of the novelties of Spin is its relatively simple specification language, Promela, as well as the powerful abilities of the model checker. The Petri net notation is a mathematical tool for modeling various classes of systems, especially those that involve concurrency and parallelism. The Honeywell Domain Modeling Environment (DOME) is a tool that supports system design using a wide variety of modeling notations, including UML diagrams and Petri nets. We describe a tool that supports the use of the Spin model checker to analyze and verify Petri net specifications that have been constructed using the DOME tool. In addition to discussing the translation of Petri nets into Promela, we present several example Petri net specifications as well as their analysis using Spin.