Validating Multiple Variants of an Automotive Light System with Electrum

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2020

Autores

Cunha, A (Autor) Outra; Macedo, N (Autor) FEUP; Liu, C (Autor) Outra

Ata de Conferência Internacional

Título: Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings

Páginas: 318-334

7th International Conference on Rigorous State-Based Methods, ABZ 2020

27 May 2020 through 29 May 2020

Indexação

Scopus - 1 Citação

Outras Informações

ID Authenticus: P-00S-6MP

DOI: 10.1007/978-3-030-48077-6_26

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

Idioma: Inglês

Tipo (Avaliação Docente): Científica