-
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 format from the case study call. The values of the CSV are converted into the provided Electrum model and tested for validity. To see the actually generated Electrum formula for the 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 is useful to, for instance, define sequences of input signals and let Electrum find possible values for the output signals. 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.