Game-based, Easy And Reverse model-checking
The current release of the plugin is version
1.0.8 known to be working with jABC version 3.6a.
- 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
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
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).
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
The authors can be contacted via e-mail: Marco Bakera
and Clemens Renner.