Helena is an explicit model checker developed at the CEDRIC research center in the CNAM university in Paris. It is a free software written in Ada available under the terms of the GNU general public license.
Helena works on a Linux platform, but a Windows version should be soon available.

Model checking is an automatic technique to verify properties of finite state systems by inspecting all the possible configurations (or states) of the system. In Helena, this system is described as a high level Petri net. In the current version, Helena can be used for the verification of state properties and deadlock freeness. When Helena finds a state that violates the specified property, the faulty execution is reported to the user. Helena is a command line oriented tool without any graphical user interface.


Helena is developped by the following people

• Christophe Pajault, PHD student at the CNAM university [homepage, email]
• Sami Evangelista, PHD student at the CNAM university [homepage, email]

Features
Helena includes the following features

• High level formalism
• Efficient firing rule
• Code generation to speed up the analysis
• Optimized state space storage method
• Structural abstractions techniques
• Partial order methods
• Interface with other Petri nets tools : Lola, Prod, Tina

Download and Further Information
In order to download Helena, go to the SourceForge summary page here. There you you can also submit bug reports, request new features to be implemented, download the documentation, join mail lists, and many other stuff.

Sample examples
As an introduction to Helena we propose the two following examples :

• The distributed database system
• The load balancing system

Papers and reports
Below is a list of some publications related to Helena.

• Christophe Pajault and Jean-François Pradat-Peyre. Distributed Colored Petri Net Model-Checking with Cyclades. 2006. in Proceedings of the 5th International Workshop on Parallel and Distributed Methods in Verification.
• Sami Evangelista and Jean-François Pradat-Peyre. On the Computation of Stubborn Sets of Colored Petri Nets. 2006. in Proceedings of the 26th International Conference on Application and Theory of Petri Nets, pages 146-165. ©Springer-Verlag, LNCS #4024.
• Sami Evangelista and Serge Haddad and Jean-François Pradat-Peyre. Syntactical Colored Petri Nets Reductions. 2005. in Proccedings of the Third International Symposium on Automated Technology for Verification and Analysis, pages 202-216. ©Springer-Verlag, LNCS #3707.
• Sami Evangelista and Jean-François Pradat-Peyre. Memory Efficient State Space Storage in Explicit Software Model Checking. 2005. in Proceedings of the 12th International SPIN Workshop on Model Checking of Software, pages 43-57. ©Springer-Verlag, LNCS #3639.
• Sami Evangelista. High Level Petri Nets Analysis with Helena. 2005. in Proceedings of the 25th International Conference on Application and Theory of Petri Nets, pages 455-464. ©Springer-Verlag, LNCS #3536.
• Sami Evangelista and Serge Haddad and Jean-François Pradat-Peyre. New Coloured Reductions for Software Validation. 2004. in Proccedings of the 7th International workshop on discrete event systems, pages 355-360.
• Sami Evangelista and Jean-François Pradat-Peyre. An Efficient Algorithm for the Enabling Test of Colored Petri Nets. 2004. in Proceedings of the 5th International Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, pages 137-156. University of AArhus, Denmark.

This list is available as a bib file here.

Links
Here are some links on other model checking or verification tools.

• Prod and Maria, two model checkers developped at the laboratory for theoretical computer science of the Helsinki university.
  
• Spin, an explicit model checker developped at Bell labs.
• Lola, a model checker for low level Petri nets which implements several reduction techniques.
• Tina, a toolbox for the edition and analysis of Petri Nets and Time Petri Nets.

You may also look at the Yahoda database which counts some verification tools.

---