A refinement relation for families of timed automata

Software Product Lines (SPLs) are families of systems that share a high number of common assets while differing in others. In component-based systems, components themselves can be SPLs, i.e., each component can be seen as a family of variations, with different interfaces and functionalities, typical...

ver descrição completa

Detalhes bibliográficos
Autor principal: Cledou, Guillermina (author)
Outros Autores: Proença, José Miguel Paiva (author), Barbosa, L. S. (author)
Formato: conferencePaper
Idioma:eng
Publicado em: 2017
Assuntos:
Texto completo:http://hdl.handle.net/1822/69307
País:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/69307
Descrição
Resumo:Software Product Lines (SPLs) are families of systems that share a high number of common assets while differing in others. In component-based systems, components themselves can be SPLs, i.e., each component can be seen as a family of variations, with different interfaces and functionalities, typically parameterized by a set of features and a feature model that specifies the valid combinations of features. This paper explores how to safely replace such families of components with more refined ones. We propose a notion of refinement for Interface Featured Timed Automata (IFTA), a formalism to model families of timed automata with support for multi-action transitions. We separate the notion of IFTA refinement into behavioral and variability refinement, i.e., the refinement of the underlying timed automata and feature model. Furthermore, we define behavioral refinement for the semantic level, i.e., transition systems, as an alternating simulation between systems, and lift this definition to IFTA refinement. We illustrate this notion with examples throughout the text and show that refinement is a pre-order and compositional.