Paper Info
Title
An automated tool for analyzing Petri nets using Spin
Abstract
The Spin model checker is a system that has beenused to model and analyze a large number of applicationsin several domains including the aerospace industry. Oneof the novelties of Spin is its relatively simple specificationlanguage, Promela, as well as the powerful abilities of themodel checker. The Petri net notation is a mathematicaltool for modeling various lasses of systems, especiallythose that involve concurrency and parallelism. TheHoneywell Domain Modeling Environment (DOME) is atool that supports system design using a wide variety ofmodeling notations, including UML diagrams and Petrinets. In this paper we describe a tool that supports theuse of the Spin model checker to analyze and verify Petrinet specifications that have been onstructed using theDOME tool. In addition to discussing the translation ofPetri nets into Promela, we present several example Petrinets specifications as well as their analysis using Spin.
Year
DOI
Venue
2001
10.1109/ASE.2001.989839
Automated Software Engineering, 2001.
Keywords
Field
DocType
Petri nets,automatic programming,formal specification,parallel programming,program verification,specification languages,DOME,Honeywell Domain Modeling Environment,Petri net analysis,Petri net notation,Petri net specifications,Promela,Spin model checker,UML diagrams,automated tool,concurrency,mathematical tool,modeling notations,parallelism,simple specification language,system design
Specification language,Programming language,Petri net,Systems engineering,Concurrency,Computer science,Process architecture,Theoretical computer science,Formal specification,Promela,Domain model,SPIN model checker
Conference
ISSN
ISBN
Citations 
1938-4300
0-7695-1426-X
15
PageRank 
References 
Authors
0.97
3
2
Name
Order
Citations
PageRank
gerald c gannod1867.76
Sunil Gupta2150.97