UNIGE document Technical Report
previous document  unige:26582  next document
add to browser collection

Properties specification language for algebraic Petri nets

Year 2010
Description 22 p.
Abstract Model Checking consists in verifying if a model of a given system meets a set of requirements. The model and the properties can be specified with various formalisms. We chose Algebraic Petri Nets (APNs), a powerful formalism used to model concurrent systems, for the model specification. This report proposes a language for defining invariant properties on APNs. The expressiveness of the language proposed is similar to first order logic, with some extensions (deadlocks and cardinalities). These properties can be used to define the requirements for model checking. This language was created for the tool AlPiNA, an APN model checker developed at the University of Geneva.
Keywords Model checkingAlgebraic Petri NetsPropertiesInvariantsSpecification languageFirst-order logicAlPiNA
Full text
Report (659 Kb) - public document Free access
Research group Software Modeling and Verification
(ISO format)
MARECHAL MARIN, Alexis Ayar, BUCHS, Didier. Properties specification language for algebraic Petri nets. 2010 https://archive-ouverte.unige.ch/unige:26582

342 hits



Deposited on : 2013-03-05

Export document
Format :
Citation style :