-
Notifications
You must be signed in to change notification settings - Fork 9
ELS
This page presents the resources relevant for the modelling and subsequent validation and verification of an Automotive Adaptive Exterior Light System (ELS) in Electrum, and was 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 the following pre-print. To handle the multiple variants of ELS, several approaches where explored, resulting in different models:
- Distinct model for each variant, effectively there are only 4 distinct variants:
- A pure Electrum model under a variability idiom
- A "colourful" Electrum model under an extension for feature annotations
The following theme can be applied to all the above models for improved visualization.
The colourful Electrum was adapted from the following publication for Alloy, and the respective version of the Analyzer is available here.
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 AdaptiveExteriorLight_multi.ele seq.csv
where seq.csv represents a validation sequence in CSV as described in the pre-print, which essentially adds a header information to the provided spreadsheet. The values of the CSV are converted into the provided Electrum model and tested for validity. The CSV may have empty cells in which case their value is left free in Electrum encoding and assigned a value during solving. This is useful to, for instance, define sequences of input signals and let Electrum find possible values for the output signals. To see the actually generated Electrum formula for the sequence, pass the option --pred to the validator; to see the resulting CSV, including the assignments to empty cells, pass the option --csv to the validator.
Below are the reference validation sequences in the accepted CSV format:
Sequence 7 has been fixed for what are, in our perspective, inconsistencies. 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.