ELS

Adaptive Exterior Light System

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.

Model for the HL3 Concept

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