Abstract
Model-driven development (MDD) and verification approaches are highly desirable in the development of (safety-critical) embedded systems, since they help to identify functional or non-functional issues from the early development stage when verification complexity is relatively lower than that of the implemented systems. Nevertheless, MDD approaches have not been widely adopted in practice mainly due to the difficulty and high initial cost of switching the development paradigm from code-centric to model-driven. This work presents a systematic method for reverse engineering abstract models from embedded codes using the notion of abstract components which act as independent units of development, validation, and verification. The recursive reverse engineering process constructs high-level abstract components from low-level ones using synchronized abstraction and projection abstraction, defined w.r.t. the information on port dependency and port bindings. This approach is demonstrated with reverse-engineered TinyOS, where each abstract component is validated and verified using model simulation and model checking.