Skip to content
nmacedo edited this page Jun 17, 2021 · 29 revisions

Adaptive Exterior Light System

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.

Model for the ELS

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):
    • EU model (==DriverPosition)
    • USA model (==Canada,==DriverPosition)
    • EU+ArmouredVehicle model (==DriverPosition)
    • USA+ArmouredVehicle model (==Canada,==DriverPosition)
  • 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.

Validation sequences

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:

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.

Scenario 1 - Normal light, no daytime light, no ambient light, day

S1_0

S1_1

S1_2

S1_3

S1_4

S1_5

S1_6

S1_7

S1_8

S1_9

S1_10

S1_11

S1_12

S1_13

S1_14

S1_15

S1_16

S1_17

Scenario 2 - Normal light, no daytime light, ambient light, night

S2_0

S2_1

S2_2

S2_3

S2_4

S2_5

S2_6

S2_7

S2_8

S2_9

S2_10

S2_11

S2_12

Scenario 3 - Normal light, daytime light, no ambient light, day

S3_0

S3_1

S3_2

S3_3

S3_4

S3_5

S3_6

S3_7

S3_8

Scenario 4 - Normal light, daytime light, ambient light, night

S4_0

S4_1

S4_2

S4_3

S4_4

S4_5

S4_6

Scenario 5 - Normal light, no daytime light, ambient light, night

S5_0

S5_1

S5_2

S5_3

S5_4

S5_5

S5_6

S5_7

Scenario 6 - Turn indicator, no daytime light

S6_0

S6_1

S6_2

S6_3

S6_4

S6_5

S6_6

S6_7

S6_8

S6_9

S6_10

S6_11

S6_12

S6_13

S6_14

S6_15

S6_16

S6_17

S6_18

S6_19

S6_20

S6_21

S6_22

S6_23

S6_24

S6_25

S6_26

S6_27

Scenario 7 - Turn indicator and Hazard light, daytime light

S7_0

S7_1

S7_2

S7_3

S7_4

S7_5

S7_6

S7_7

S7_8

S7_9

S7_10

S7_11

S7_12

S7_13

S7_14

S7_15

S7_16

S7_17

S7_18

Scenario 8 - Manual high beam

S8_0

S8_1

S8_2

S8_3

S8_4

S8_5

S8_6

S8_7

Scenario 9 - Adaptive high beam, no cruise control

S9_0

S9_1

S9_2

S9_3

S9_4

S9_5

S9_6

S9_7

S9_8

S9_9

S9_10

S9_11

S9_12

S9_13