Model Checking

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 …

BMoth

A prototypical model checker focussing on reusable libraries.

Formal Methods Accessibility

Lower barriers and learning curves to enable the usage of formal methods in mainstream industries.

ProB

Animator, constraint solver and (symbolic) model checker for the B-Method.