In: Gianfranco Ciardo, Philippe Darondeau (Eds.): Lecture Notes in Computer Science, Vol. 3536: Applications and Theory of Petri Nets 2005: 26th International Conference, ICATPN 2005, Miami, USA, June 20-25, 2005., pages 455-464. Springer Verlag, June 2005.
Abstract: 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.