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

Hello for my Master's dissertation I did a project on model checking Event-B. After spending 3 months on this I am unwilling to just let go of it.

This project can be used to model check Event-B machines through a Rodin Plugin. It uses automata-based model checking and can be applied to finite as well as infinite executions.

I will admit that there are currently performance issues that appear to come from the construction of the automata.