ELS
Safety and comfort functions in modern cars are often realized in software running on several electronic control units (ECUs) that connect actuators and sensors. Besides the complexity of such distributed system, such systems must additionally be configurable for different markets or customer preferences.
The described Adaptive Exterior Light System (ELS) for the automotive domain integrates essential functions such as the headlights and the turn signals, but also comfort functions such as cornering lights. It receives information both from the user interface (switches, pitman arms, setting menu, etc) and a series of sensors (key position, brightness sensor, steering wheel, etc) and activates the lighting actuators. Different configuration may enable different functions altogether or modify their behaviour.
This page presents the resources relevant for the modelling and subsequent validation and verification of the proposed ELS in Electrum, developed as an answer to the ABZ 2020 call for case study contributions, mainly based on the reference document v1.17 and the validation sequences v1.8.
The Electrum models for the ELS are presented in detail in the ABZ'20 paper. To handle the multiple variants of ELS, several approaches where explored, resulting in different models:
- Distinct Electrum model for each variant (there are only 4 effectively distinct variants):
- A single model in pure Electrum under a variability idiom
- A single "colourful" Electrum model under an extension for feature annotations.
The following theme can be applied to all the above models for improved visualisation in the Electrum Analyzer.
The colourful Electrum was adapted from the following publication for Alloy, and an experimental version of the Analyzer is available here.
Note: While these models were initially developed for Electrum 2.0, they have been updated for Electrum 2.1 in order to be analysable by the latest version of the tool, except for the colorful model since the prototype Analyzer was not updated to Electrum 2.1.
A validator for the reference validation sequences has been developed that converts CSV sequences into Electrum and back. To use it simply run from the command line:
java -jar els-validator-v0.1.jar els_multi.ele seq.csv
where seq.csv represents a validation sequence in CSV as described in the paper, which essentially adds header information to the provided spreadsheet format from the case study call. The values of the CSV file are converted into the provided Electrum model and tested for validity. To inspect the actually generated Electrum formula for the provided sequence, pass the option --pred to the validator.
If cells are left empty in the CSV their values will be free in the Electrum encoding and solved during analysis. This allows domain experts to define sequences of input signals, let Electrum find acceptable values for the output signals, and then validate the results. To see the solutions back into CSV, including the assignments to empty cells, pass the option --csv to the validator.
Below are the 9 reference validation sequences in the accepted CSV format:
- Validation sequence 1
- Validation sequence 2
- Validation sequence 3
- Validation sequence 4
- Validation sequence 5
- Validation sequence 6
- Validation sequence 7
- Validation sequence 8
- Validation sequence 9
Sequence 7 has been fixed for what are, in our perspective, inconsistencies with the requirements. Sequence 9 has been adapted due to the lack of arithmetic support of our approach. The Electrum encoding for the sequences has also been integrated in the models provided above for validation within the Analyzer.
Some of these sequences, but with only the input signals defined, are also available to demonstrate the generation of expected outputs:
Validation sequences can also be animated and inspected in the visualiser of the Electrum Analyzer. Below is the result of these scenarios, under the theme shared above.
