EbChecker

Created: 2012/11/08 20:27:15+0000 Revised: 2012/11/08 20:27:15+0000 Revisions:  4 3 2 1

I graduated from the University of Southampton with a Master's degree in Software Engineering. My dissertation presented an automata-based explicit model checker for Event-B. Event-B is based on the B Method and is a formal specification language. I implemented the model checker as a plugin for Rodin, a development environment for Event-B based on Eclipse.

The code is available from a BitBucket repository https://bitbucket.org/mattunderscorechampion/modelchecker. There is a dependency on the LTL2BA4JOSGi project which is used to construct specification automata. I intend to make this available through an update site as soon as I can.