A Formal Modeling and Analysis Framework for Software Product Line of Preemptive Real-Time Systems
(2016) Symposium on Applied Computing — Location: Pisa, Italy (4.April.2016)
Files
No attached file found for this publication.
Details
- Authors
- 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.
- Affiliations
Citations
Kim Jin, H., Legay, A., Traonouez, L.-M., Acher, M., & Kang, S. (2016). A Formal Modeling and Analysis Framework for Software Product Line of Preemptive Real-Time Systems. Proceedings of the 31st Annual ACM Symposium on Applied Computing - SAC ’16. Published. Symposium on Applied Computing, Pisa, Italy. https://doi.org/10.1145/2851613.2851977