Behavioural modelling and verification of real-time software product lines

Research output: Contribution in Book/Catalog/Report/Conference proceedingChapter

116 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the 16th International Software Product Line Conference (SPLC '12), Salvador, Brazil, September 2-7
Pages66-75
Number of pages10
Volume1
DOIs
Publication statusPublished - 2012

Fingerprint

Model checking
Formal methods
Software engineering

Cite this

Cordy, M., Schobbens, P-Y., Heymans, P., & Legay, A. (2012). Behavioural modelling and verification of real-time software product lines. In Proceedings of the 16th International Software Product Line Conference (SPLC '12), Salvador, Brazil, September 2-7 (Vol. 1, pp. 66-75) https://doi.org/10.1145/2362536.2362549
Cordy, Maxime ; Schobbens, Pierre-Yves ; Heymans, Patrick ; Legay, Axel. / Behavioural modelling and verification of real-time software product lines. Proceedings of the 16th International Software Product Line Conference (SPLC '12), Salvador, Brazil, September 2-7. Vol. 1 2012. pp. 66-75
@inbook{a81d312a0e6d49bf9f56ff16a884f5d8,
title = "Behavioural modelling and verification of real-time software product lines",
abstract = "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 {\circledC} 2012 ACM.",
author = "Maxime Cordy and Pierre-Yves Schobbens and Patrick Heymans and Axel Legay",
year = "2012",
doi = "10.1145/2362536.2362549",
language = "English",
isbn = "9781450310956",
volume = "1",
pages = "66--75",
booktitle = "Proceedings of the 16th International Software Product Line Conference (SPLC '12), Salvador, Brazil, September 2-7",

}

Cordy, M, Schobbens, P-Y, Heymans, P & Legay, A 2012, Behavioural modelling and verification of real-time software product lines. in Proceedings of the 16th International Software Product Line Conference (SPLC '12), Salvador, Brazil, September 2-7. vol. 1, pp. 66-75. https://doi.org/10.1145/2362536.2362549

Behavioural modelling and verification of real-time software product lines. / Cordy, Maxime; Schobbens, Pierre-Yves; Heymans, Patrick; Legay, Axel.

Proceedings of the 16th International Software Product Line Conference (SPLC '12), Salvador, Brazil, September 2-7. Vol. 1 2012. p. 66-75.

Research output: Contribution in Book/Catalog/Report/Conference proceedingChapter

TY - CHAP

T1 - Behavioural modelling and verification of real-time software product lines

AU - Cordy, Maxime

AU - Schobbens, Pierre-Yves

AU - Heymans, Patrick

AU - Legay, Axel

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84867484666&partnerID=8YFLogxK

U2 - 10.1145/2362536.2362549

DO - 10.1145/2362536.2362549

M3 - Chapter

SN - 9781450310956

VL - 1

SP - 66

EP - 75

BT - Proceedings of the 16th International Software Product Line Conference (SPLC '12), Salvador, Brazil, September 2-7

ER -

Cordy M, Schobbens P-Y, Heymans P, Legay A. Behavioural modelling and verification of real-time software product lines. In Proceedings of the 16th International Software Product Line Conference (SPLC '12), Salvador, Brazil, September 2-7. Vol. 1. 2012. p. 66-75 https://doi.org/10.1145/2362536.2362549