High level Petri nets analysis with Helena. This paper presents the high level Petri nets analyzer Helena. Helena can be used for the on-the-fly verification of state properties, i.e., properties that must hold in all the reachable states of the system, and deadlock freeness. Some features of Helena make it particularly efficient in terms of memory management. Structural abstractions techniques, mainly transitions agglomerations, are used to tackle the state explosion problem. Benchmarks are presented which compare our tool to Maria. Helena is developed in portable Ada and is freely available under the conditions of the GNU General Public License.
Keywords for this software
References in zbMATH (referenced in 11 articles , 1 standard article )
Showing results 1 to 11 of 11.
- Pommereau, Franck: SNAKES: a flexible high-level Petri nets library (tool paper) (2015)
- Choppy, Christine; Dedova, Anna; Evangelista, Sami; Klaï, Kaïs; Petrucci, Laure; Youcef, Samir: Modelling and formal verification of the NEO protocol (2012) ioport
- Kordon, Fabrice; Linard, Alban; Buchs, Didier; Colange, Maximilien; Evangelista, Sami; Lampka, Kai; Lohmann, Niels; Paviot-Adet, Emmanuel; Thierry-Mieg, Yann; Wimmel, Harro: Report on the model checking contest at Petri nets 2011 (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
- Evangelista, Sami; Pajault, Christophe: Solving the ignoring problem for partial order reduction (2010) ioport
- Bashirov, Rza; Kordon, Fabrice; Lort, Hüseyin: Exploiting colored Petri nets to decide on permutation admissibility (2009)
- Bouroulet, Roland; Devillers, Raymond; Klaudel, Hanna; Pelz, Elisabeth; Pommereau, Franck: Modeling and analysis of security protocols using role based specifications and Petri nets (2008)
- Klaudel, Hanna; Koutny, Maciej; Pelz, Elisabeth; Pommereau, Franck: Towards efficient verification of systems with dynamic process creation (2008)
- Evangelista, Sami; Pradat-Peyre, Jean-François: On the computation of stubborn sets of colored Petri nets (2006)
- Evangelista, Sami: High level Petri nets analysis with Helena (2005)
- Evangelista, Sami; Pradat-Peyre, Jean-François: Memory efficient state space storage in explicit software model checking (2005)