Helena is an explicit model checker. It is a free software written in Ada available under the terms of the GNU general public license.
Helena works on a Linux platform.

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 graphical interface.

Helena is developped by the following people

• Sami Evangelista [homepage]
• Christophe Pajault [homepage]

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 following examples.

• The distributed database system
• The load balancing system
• The towers of Hanoi

Links
Here are some links to 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.

---