A Formal Modeling and Analysis Framework for Software Product Line of Preemptive Real-Time Systems

Jin Hyun Kim 1 Axel Legay 1 Louis-Marie Traonouez 1 Mathieu Acher 2, 3 Sungwon Kang 4
1 TAMIS - Threat Analysis and Mitigation for Information Security
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
2 DiverSe - Diversity-centric Software Engineering
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper presents a formal analysis framework to analyze a family of platform products w.r.t. real-time properties. First, we propose an extension of the widely-used feature model, called Property Feature Model (PFM), that distinguishes features and properties explicitly Second, we present formal behavioral models of components of a real-time scheduling unit such that all real-time scheduling units implied by a PFM are automatically composed to be analyzed against the properties given by the PFM. We apply our approach to the verification of the schedulability of a family of scheduling units using the symbolic and statistical model checkers of Uppaal.
Complete list of metadatas

Cited literature [8 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01241673
Contributor : Louis-Marie Traonouez <>
Submitted on : Friday, October 28, 2016 - 11:56:03 AM
Last modification on : Thursday, February 7, 2019 - 2:33:08 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

Jin Hyun Kim, Axel Legay, Louis-Marie Traonouez, Mathieu Acher, Sungwon Kang. A Formal Modeling and Analysis Framework for Software Product Line of Preemptive Real-Time Systems. Symposium on Applied Computing, Apr 2016, Pise, Italy. pp.1562 - 1565, ⟨10.1145/2851613.2851977⟩. ⟨hal-01241673v2⟩

Share

Metrics

Record views

882

Files downloads

409