HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [8 references]  Display  Hide  Download

Contributor : Louis-Marie Traonouez Connect in order to contact the contributor
Submitted on : Friday, October 28, 2016 - 11:56:03 AM
Last modification on : Thursday, January 20, 2022 - 5:29:41 PM


Files produced by the author(s)



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⟩



Record views


Files downloads