Validating multiple variants of an automotive light system with Alloy 6

• DOI: 10.1007/s10009-024-00752-3
• Publication Date: 2024-05-23T07:01:56Z
• Authors: Alcino Cunha; Nuno Macedo; Chong Liu
• Keywords: Theory of computation

Abstract This paper reports on the development and validation of a formal model for an automotive adaptive exterior lights system (ELS) with multiple variants in 6, which is most recent version lightweight specification language that supports mutable relations temporal logic. We explore different strategies to address variability, one pure another through annotative extension. then show how its can be used validate systems this nature, namely by checking reference scenarios are admissible, automatically verify whether established requirements hold. A prototype was developed translate provided sequences into back further automate process. The resulting ELS validated against verified all variants.