A High-level specification language for model checking

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


PhD project by Signe Geisler Pedersen

Research Section: Software and Process Engineering

Principal Supervisor: Anne Elisabeth Haxthausen

Co-supervisor: Jan Peleska

Title of Project: A High-level Specification Language for Model Checking

Project start: 01/09/2018 → 31/08/2021


Anne Elisabeth Haxthausen
Associate Professor
DTU Compute
+45 45 25 75 10