User Guide

Created: 2012/11/21 16:47:39+0000

The use of EbChecker is simple. To start EbChecker right click on a machine in the project explorer menu. It may take several seconds during which Rodin is unresponsive to start the first time. This will bring up a window that allows you to start model checking an Event-B machine. It allows entry of LTL[e] formula to evaluate a machine and select an algorithm to use when model checking. After selecting 'Start Model Checking' the model checking algorithm is applied. The time this takes will depend on the size of the model. Due to early stage implementation of EbChecker it is advised that only small models are checked. Rodin will be unresponsive whilst it is run. Refer to the sections on background information for a better understanding of how this works. After it has completed it will display a window with the results of the model checking. It will report if the model satisfies the specification, the size of the model and the time taken to explore it. If a counterexample to the specification is found this will be reported in a separate window. It will present a tree, each root item will be the event fired to reach that state, each subitem is part of the state after the event has been fired. The items are colour coded so that the states that violate the specification are displayed in red and all other states are displayed in blue.