Signe Geisler Pedersen: There is a growing reliance on software systems. Many of these are safety critical and therefore, it is essential to ensure their correctness and reliability. An example of such a system is a railway control system.
Ensuring correctness of a system can
be achieved through the use of
formal methods, which are mathematically based
methods for modelling and analysing computer systems, e.g. with respect to safety
properties. This project will focus on the formal verification method
model checking,
which has shown useful for automated verification of state-based systems.
When applying model checking, a model of the system to be verified should
be specified along with the desired properties (e.g. safety) of the system. The
specification of the model and properties is then used as input for a model checking
tool, which will determine whether the model satisfies the properties. There exist
several different model checking tools, which are optimised for different types of
systems and, in effect, have different advantages and disadvantages. Typically, there
is a separate specification language, or
input language, for each model checking tool,
many of which lack expressive power. For these reasons, it is often problematic to
make the choice between the model checkers for a specific application.
It would be useful to be able to compare the efficiency of different model checkers
on the same system without having to rewrite the specifications in another input
language. This could be achieved by having a
common input language
for multiple
model checkers, which could additionally provide
enhanced expressive power.
This project aims to create such a high level common input language. The
language will act as a ”front-end” for several different model checker back-ends,
allowing the utilisation and comparison of different model checkers using a single
input language. The language should facilitate the specification of generic models
and configuration of these to support efficient specification and model checking
of families of systems. Additionally, a method for encapsulating the language in
domain-specific languages should be developed. Domain-specific languages can hide
the use of formal methods for domain experts and use the terms and concepts of the
domain, allowing the domain experts (who are not necessarily familiar with formal
methods) to more easily construct and understand system specifications.
PhD project title: A High-level Specification Language for Model Checking
Effective start/end date 01/09/2018 → 31/08/2021
Supervised by Anne Haxthausen, section for Software and Process Engineering