About MOVIDA Model Checker

The Model Checker tool can be used compute state spaces for TNCES and run model checking on them. The Model Checker is one of the MOVIDA tools and it can be invoked from the NCES Analyzer.

The model checker application has a graphical user interface that is divided into three parts: the main GUI, the Unconnected Transitions GUI and the Formulae list GUI. In the main GUI the user can load TNCES and compute state spaces for them. The TNCES can then be configured using the Unconnected transitions GUI. State spaces can also be saved to a file or loaded from a file. Once a state space has been obtained the user can start the Formulae list GUI to perform model checking.

The properties of the models are expressed using Computation Tree Logic or CTL. The entered formulas must strictly follow a specified syntax.