We propose a model-based framework for developing a self- adaptive embedded program, which monitors its own execu- tion 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 devel- oping 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 recon- figuration specification language REDL to specify reconfig- uration requirements, and define a formal semantics of re- configuration in context of hybrid automaton. Using formal methods also helps automate design and implementation: we use model-based runtime verification techniques intro- duced in [19] to extend a system model to a self-monitoring model based on its temporal logic requirements; we then ex- tend the self-monitoring model with a reconfiguration mech- anism based on its REDL specification. Our approach works with models, and hence it may be incorporated into exist- ing 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 pro- gram for targeted platform.