Case Study

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 …

Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains

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, an evolution of the ETCS Level 2 principles, introduces Virtual …

Towards Infinite-State Symbolic Model Checking for B and Event-B

The idea of verifying the correctness of software has been brought up in the early days of computing, for example by Alan Turing in 1949 or Robert W. Floyd in 1967. James C. King extended upon the idea of manual verification by suggesting and working …

Turning Failure into Proof: The ProB Disprover for B and Event-B

The ProB disprover uses constraint solving to find counter-examples for B proof obligations. As the ProB kernel is now capable of determining whether a search was exhaustive, one can also use the disprover as a prover. In this paper, we explain how …

Turning Failure into Proof: Evaluating the ProB Disprover

The ProB disprover uses constraint solving to try and find counter examples to proof obligations. As the ProB kernel is now capable of determining whether a search was exhaustive, one can also use the disprover as a prover. In this paper, we compare …