Model-Based Self-Adaptive Embedded Programs with Temporal Logic Specifications

We propose a model-based framework for developing a self-adaptive embedded program, which monitors its own execution and reconfigures itself at runtime to avoid failure and improve performance. Our approach uses formal methods at different design stages to reduce the complexity of developing a self-adaptive embedded program. In our framework system requirement is rigidly encoded in temporal logics, and the original embedded system behavior is captured in a hybrid automaton-based model. We introduce the reconfiguration specification language REDL to specify reconfiguration requirements, and define a formal semantics of reconfiguration in context of hybrid automaton. Using formal methods also helps automate design and implementation: we use model-based runtime verification techniques introduced by Tan et al. (2001) to extend a system model to a self-monitoring model based on its temporal logic requirements; we then extend the self-monitoring model with a reconfiguration mechanism based on its REDL specification. Our approach works with models, and hence it may be incorporated into existing model-based design workflow: the resulting self-adaptive model can be analyzed using an existing model simulator and may be used to generate a self-adaptive embedded program for targeted platform