Paper Info
Title
An event-based approach for formally verifying runtime adaptive real-time systems
Abstract
Real-time and embedded systems are required to adapt their behavior and structure to runtime unpredicted changes in order to maintain their feasibility and usefulness. These systems are generally more difficult to specify and verify owning to their execution complexity. Hence, ensuring the high-level design and the early verification of system adaptation at runtime is very crucial. However, existing runtime model-based approaches for adaptive real-time and embedded systems suffer from shortcoming linked to efficiently and correctly managing the adaptive system behavior, especially that a formal verification is not allowed by modeling languages such as UML and MARTE profile. Moreover, reasoning about the correctness and the precision of high-level models is a complex task without the appropriate tool support. In this work, we propose an MDE-based framework for the specification and the verification of runtime adaptive real-time and embedded systems. Our approach stands for Event-B method to formally verify resources behavior and real-time constraints. In fact, thanks to MDE M2T transformations, our proposal translates runtime models into Event-B specifications to ensure the correctness of runtime adaptive system properties, temporal constrains and nonfunctional properties using Rodin platform. A flood prediction system case study is adopted for the validation of our proposal.
Year
DOI
Venue
2021
10.1007/s11227-020-03386-9
The Journal of Supercomputing
Keywords
DocType
Volume
Adaptation, Real-time and embedded systems, Runtime context, MARTE, Event-B method, M2T transformation
Journal
77
Issue
ISSN
Citations 
3
0920-8542
1
PageRank 
References 
Authors
0.37
15
3
Name
Order
Citations
PageRank
Nissaf Fredj110.37
Yessine Hadj Kacem2349.72
Abid Mohamed33919.08