Adaptive Exterior Light and Speed Control System (ABZ 2020)
This document describes two systems from the automotive domain: an adaptive exterior light system (ELS) and a speed control system (SCS). This specification is based on the SPES XT running example. Besides their general architectures, the requirements of the software based controllers are described. Both systems are only loosely coupled, which makes it possible to handle them independently
Publications
A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
Abstract 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) approach following a formal method, we use MISRA C for a low-level implementation instead.
An Event-B Model of an Automotive Adaptive Exterior Light System
Abstract This paper introduces an Event-B formal model of the adaptive exterior light system for cars, a case study proposed in the context of the ABZ2020 conference. The system describes the different provided lights and the conditions under which they are switched on/off in order to improve the visibility of the driver without dazzling the oncoming ones.
Modeling of a Speed Control System using Event-B
Abstract The present paper presents our proposal of an Event-B model of a speed control system, a part of the case study provided in the ABZ2020 conference. The case study describes how the system regulates the current speed of a car according to a set criteria like the speed desired by the driver, the position of a possible preceding vehicle but also a given speed limit that the driver must not exceed.
Modelling an automotive software-intensive system with adaptive features using ASMETA
Abstract In the context of automotive domain, modern control systems are software-intensive and have adaptive features to provide safety and comfort. These software-based features demand software engineering approaches and formal methods that are able to guarantee correct operation, since malfunctions may cause harm/damage.
Modelling and Validating an Automotive System in Classical B and Event-B
Abstract We have modelled parts of the ABZ automotive case study using the B-method. For the early phases of modelling we have used the classical B for software, while for proof we have used Event-B and Rodin.
Validating Multiple Variants of an Automotive Light System with Electrum
Abstract This paper reports on the development and validation of a formal model for an automotive adaptive exterior lights system (ELS) with multiple variants in Electrum, a lightweight formal specification language that extends Alloy with mutable relations and temporal logic.
Adaptive Exterior Light and Speed Control System
Abstract This case study continues the successful series of case studies for formal specification and verification of the ABZ conference series, which started with the landing gear system and expanded with the hemodialysis medical device and the European Train Control System (ETCS) in the following years.