Behavioural modelling and verification of real-time software product lines

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceChapitre

131 Téléchargements (Pure)


In Software Product Line (SPL) engineering, software products are build in families rather than individually. Many critical software are nowadays build as SPLs and most of them obey hard real-time requirements. Formal methods for verifying SPLs are thus crucial and actively studied. The verification problem for SPL is, however, more complicated than for individual systems; the large number of different software products multiplies the complexity of SPL modelchecking. Recently, promising model-checking approaches have been developed specifically for SPLs. They leverage the commonality between the products to reduce the verification effort. However, none of them considers real time. In this paper, we combine existing SPL verification methods with established model-checking procedures for realtime systems. We introduce Featured Timed Automata (FTA), a formalism that extends the classical Timed Automata with constructs for modelling variability. We show that FTA model-checking can be achieved through a smart combination of real-time and SPL model checking. Copyright © 2012 ACM.
langue originaleAnglais
titreProceedings of the 16th International Software Product Line Conference (SPLC '12), Salvador, Brazil, September 2-7
Nombre de pages10
Les DOIs
Etat de la publicationPublié - 2012

Empreinte digitale

Examiner les sujets de recherche de « Behavioural modelling and verification of real-time software product lines ». Ensemble, ils forment une empreinte digitale unique.
  • Evolution: PReCISE Evolution

    Cleve, A.


    Projet: Axe de recherche

Contient cette citation