Validating multiple variants of an automotive light system with Alloy 6

• Tipo: Artigo em Revista Científica Internacional
• Data: 2024

Autores

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

Revista

Título: International Journal on Software Tools for Technology Transfer

Vol. 26

Páginas: 365-377

ISSN: 1433-2779

Editora: Springer Nature

Indexação

ISI Web of Knowledge - 0 Citações

Scopus - 0 Citações

Outras Informações

ID Authenticus: P-010-HRM

DOI: 10.1007/s10009-024-00752-3

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 Alloy 6, which is the most recent version of the Alloy lightweight formal specification language that supports mutable relations and temporal logic. We explore different strategies to address variability, one in pure Alloy and another through an annotative language extension. We then show how Alloy 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 Alloy 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.

Idioma: Inglês

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

Nº de páginas: 13