GEAR Game-based, Easy And Reverse model-checking

Release status

The current release of the plugin is version 1.0.8 known to be working with jABC version 3.6a.

Key Features

• Full integration into the jABC-platform for completely graphical usage as well as full usage by a command line interface.
• Reverse checking: find the sub-formulas satisfied at a given node.
• Full integration with the FormulaBuilder plugin.
• Easy maintenance of formulas and descriptions.
• Extensibility of the model to be used for the model checking process by implementing simple Java interfaces (sample implementations are a CSV-based format and of course the SIB Graph model).
• Easy usage of the plugin by providing seperate views on the model checking process (namely an advanced and a basic view).
• Supported temporal logics cover full modal μ -calculus and CTL.
• Visualization and interaction of underlying game-based algorithm as SIB-Graph.
• Powerful macro mechanism capable of enhancing the syntax with arbitrary operators (even actual alternative model-checking algorithms), thus turning GEAR into a model-checking framework.

Documentation & Resources

Manual

Flash Tutorials

Java API (Core)

Java API (GUI)

Version History

Project Details

GEAR has some additional documentation on its jETI integration in the FMICS project Wiki (English) and some implementation details and developer notes in the Java ABC Wiki (German).

Getting support

Any support requests should be sent to the GEAR mailing list which is also very suitable for discussion among the GEAR users and developers. We also provide a bug tracker for those who would like to report problems or make feature requests (registration required).

Getting GEAR

GEAR is currently not available as a public release.

If you are interested in obtaining the Java ABC Framework along with this plugin, please contact Ralf Nagel.

Last updated: $Date: 2008-05-21 11:07:04 +0200 (Wed, 21 May 2008) $.
GEAR and its webpage use images based on the Tango Desktop Project (License Details).

The authors can be contacted via e-mail: Marco Bakera and Clemens Renner.