The GEAR model checker

During my studies at the University of Dortmund (today Dortmund University of Technology), I have been working on the GEAR model checker, together with Marco Bakera. A model checker is a tool that helps you identify problems with an IT application. The application can be a web service (like Google Mail), a traditional computer program (like a word processor) or a piece of electronic hardware (like a computer-controlled elevator). Most model checkers work by first creating an abstract representation of the application (the model). Then they check whether the application's model is valid with respect to a given requirement (a property). It's fairly easy to see that this gives rise to a lot of new problems. The first issue is the generation of the model. Some information about the application is usually lost in this process. The next hard part lies in the property. These can look like this AG EF good or even as ugly (at least to most people) like this ν Z (μ X. good ∨ <a>X) ∧ [b]Z With the GEAR model checker, we have integrated the model checking process at a place where there is no need for model generation because the users of the development environment already build their programs on an abstract level – they are actually modelling it. As far as the creation of properties go, this job can be delegated to people who know how to write them and the one who builds the application can concentrate on the actual development.

Project links