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 lasses 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. In this paper we describe a tool that supports the use of the Spin model checker to analyze and verify Petri net specifications that have been onstructed using the DOME tool. In addition to discussing the translation of Petri nets into Promela, we present several example Petri nets specifications as well as their analysis using Spin.