A Formal Modeling and Analysis Framework for Software Product Line of Preemptive Real-Time Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

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

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (972.94 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01241673 , version 1 (11-12-2015)
hal-01241673 , version 2 (28-10-2016)

Identifiants

Citer

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⟩
813 Consultations
313 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More