Description

Model checking is as good as the models you make: if your models to not reflect reality, then the results of the analysis (eg via model checking) are not useful. Thus, model validation is an important task. It is also time consuming, and, since similar properties are verified many times, there is room for automation here.

The purpose of this assignment is  to make model validation easier, by checking a number of properties fully automatically: are all locations reachable? Can time always progress? Is the model input-enabled? Can time progress, even in a worse-case environment?

These questions can be checked automatically, but their formulation in terms of model queries (posed eg in temporal logic) depend on the model. Thus, this project aims at formulating a list of validation properties, implement these in a model checker, eg in Uppaal.