EbChecker

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

EbChecker is a model checker for Event-B which can be installed as a plugin for the Rodin development environment. It is automata based and has support for LTL[e]. To support LTL[e] it must also represent the event used to reach a state. To support finite models in automata it introduces the idea of a terminal state a transition to is added for all states without transitions. It supports multiple emptiness checking algorithms and will be extended to include others. There are also performance improvements that can be made. It currently uses the ProB animator to calculate the next state of an Event-B machine. The ProB animator communicates with the model checker through a socket, which is where I believe a substantial performance improvements can be made. This project does not attempt to solve the state space explosion problem.