@inproceedings{a86f4bcd8f2e4268bae349dc9810fe66,
title = "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. The system can be viewed as a lights controller that reads different information form the available sensors (key state, exterior luminosity, etc.) and takes the adequate actions by acting on the actuators of the lights in order to ensure a good visibility for the driver according to the information read. Our model is built using stepwise refinement with the Event-B method. We consider all the features of the case study, all proof obligations have been discharged using the Rodin provers. Our model has been validated using ProB by applying the different provided scenarios. This validation has permitted us to point out and correct some mistakes, ambiguities and oversights in the first versions of the case study.",
keywords = "Adaptive exterior light system, Event-B method, Refinement, Verification",
author = "Amel Mammar and Marc Frappier and R{\'e}gine Laleau",
note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2020.; 7th International Conference on Rigorous State-Based Methods, ABZ 2020 ; Conference date: 27-05-2020 Through 29-05-2020",
year = "2020",
month = jan,
day = "1",
doi = "10.1007/978-3-030-48077-6\_28",
language = "English",
isbn = "9783030480769",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "351--366",
editor = "Alexander Raschke and Dominique M{\'e}ry and Frank Houdek",
booktitle = "Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings",
}