Created: 2012/11/08 20:27:15+0000 Revised: 2012/12/15 18:02:43+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 which I have taken to calling EbChecker. 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. These have been made available through an update site and a subdomain has been devoted to this project.

For those of you interested in linked data for this project, see here: