Li Tan. In the proceedings of the 6th IEEE International Conference on Quality Software (QSIC'06). Beijing, China., October 27-28, 2006.
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 a reconfiguration specification language \redl\ to specify reconfiguration requirements, and define a formal semantics of reconfiguration in context of hybrid automaton. Using formal methods also help automate design and implementation: we use model-based runtime verification techniques introduced in \cite{TanKim04} 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.