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 become a necessity.
Case Study
A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
ABZ 2021 – 8th International Conference on Rigorous State Based Methods, virtual
Testing, Model Checking and Static Analysis – Dream Team or Rivals?
Ensuring reliability and quality of software has become a necessity.
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 instead.
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.
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.
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.
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.
Turning Failure into Proof: Evaluating the ProB Disprover
The ProB disprover uses constraint solving to try and find counter examples to proof obligations.