Validation of GSPN and SWN models through the PROD tool This paper presents an extension of the GreatSPN tool for Generalized stochastic Petri nets (GSPN) and Stochastic well-formed nets (SWN) solution that allows a check of state space properties: the extension is based on a translation of GSPN and SWN nets in GreatSPN format into high level Petri nets that are a valid input to the validation tool PROD and on a definition of a number of “analysis” macros that can be used by non-PROD experts to validate the model.
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
- Choppy, Christine; Dedova, Anna; Evangelista, Sami; Klaï, Kaïs; Petrucci, Laure; Youcef, Samir: Modelling and formal verification of the NEO protocol (2012) ioport
- Choppy, Christine; Dedova, Anna; Evangelista, Sami; Hong, Silien; Klai, Kais; Petrucci, Laure: The NEO protocol for large-scale distributed database systems: modelling and initial verification (2010) ioport
- Varpaaniemi, Kimmo; Ojala, Leo: Modelling and simulation of quantum teleportation and dense coding using predicate/transition-nets (2008)
- Latvala, Timo; Mäkelä, Marko: LTL model checking for modular Petri nets (2004)
- Aalto, Annikka; Husberg, Nisse; Varpaaniemi, Kimmo: Automatic formal model generation and analysis of SDL (2003)
- Heljanko, Keijo; Niemelä, Ilkka: Bounded LTL model checking with stable models (2003)
- Donatelli, Susanna; Ferro, Liliana: Validation of GSPN and SWN models through the PROD tool (2002)
- Esparza, Javier; Heljanko, Keijo: Implementing LTL model checking with net unfoldings (2001)
- Tauriainen, Heikki; Heljanko, Keijo: Testing Spin’s LTL formula conversion into Büchi automata with randomly generated input (2000)
- Yakovlev, A.V.; Koelmans, A.M.; Semenov, A.; Kinniment, D.J.: Modelling, analysis and synthesis of asynchronous control circuits using Petri nets (1996)