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. Adaptive Exterior Light and the Speed Control Systems are examples
of software-intensive systems that equip modern cars. We have used the Abstract State Machines to model the behaviour of both
control systems. Each model has been developed through model refinement, following the incremental way in which functional
requirements are given. We used the \asmeta tool-set to support the simulation of the abstract models, their validation against
the informal requirements, and the verification of behavioural properties. In this paper, we discuss our modelling, validation
and verification strategies, and the results (in terms of features addressed and not) of our activities. In particular, we
provide insights on how we addressed the adaptive features (the adaptive high beam headlights and the adaptive cruise control)
by explicitly modelling their software control loops according to the MAPE-K (Monitor-Analyse-Plan-Execute over a shared Knowledge)
reference control model for self-adaptive systems.
[download the pdf file] [DOI]