Model Checking

A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System

Paper presentation.

Testing, Model Checking and Static Analysis – Dream Team or Rivals?

Paper presentation.

Testing, Model Checking and Static Analysis – Dream Team or Rivals?

Ensuring reliability and quality of software has become a necessity. This is especially true for safety critical systems. To do so, different techniques have been established in industry and academia. For instance, coding guidelines such as the MISRA …

A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System

In this article, we present an approach to the ABZ 2020 case study, that differs from the ones usually presented at ABZ: Rather than using a (correct-by-construction) pproach following a formal method, we use MISRA C for a low-level implementation …

Validation and Real-Life Demonstration of ETCS Hybrid Level 3 Principles Using a Formal B Model

In this article, we present a concrete realisation of the ETCS Hybrid Level 3 concept, whose practical viability was evaluated in a field demonstration in 2017. Hybrid Level 3 introduces virtual sub-sections as sub-divisions of classical track …

Translating Alloy and Extensions to Classical B

In this article, we introduce a denotational translation of the specification language Alloy to classical B. Our translation closely follows the Alloy grammar. Each construct is translated into a semantically equivalent component of the B language. …

Prototyping Games using Formal Methods

Paper presentation.

Inquiry- and Research-based Teaching in a Course on Model Checking

Paper presentation.

Inquiry- and Research-based Teaching in a Course on Model Checking

In this presentation, we discuss a recent publication on our course on model checking. The course has been shifted from a classical lecture-based format to inquiry and research-based teaching. In the article to be presented, we documented course …

Experience Report on An Inquiry-Based Course on Model Checking

The development and improvement of model checkers for the validation of hard- and software is an ongoing research topic in computer science. Model checking research connects theoretical and practical aspects; new algorithms are often implemented …