Case Study

Analyzing Security Aspects of Software Architectures
As the consequences of cyber attacks are becoming increasingly severe, ensuring the security of safety critical embedded software has …
A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
Paper presentation.
Jun 10, 2021 10:25 AM — 10:50 AM virtual
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, …
PDF Slides
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 …
PDF Slides
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 …
Project
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 …
PDF Cite Project DOI
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 …
PDF Cite Project
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 …
PDF Cite Project DOI
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 …
PDF Cite Project