TY - GEN
T1 - Reverse engineering abstract components for model-based development and verification of embedded software
AU - Choi, Yunja
AU - Jang, Hoon
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=79951872794&partnerID=8YFLogxK
U2 - 10.1109/HASE.2010.20
DO - 10.1109/HASE.2010.20
M3 - Conference contribution
AN - SCOPUS:79951872794
SN - 9780769542928
T3 - Proceedings of IEEE International Symposium on High Assurance Systems Engineering
SP - 122
EP - 131
BT - Proceedings - 2010 IEEE 12th International Symposium on High Assurance Systems Engineering, HASE 2010
T2 - 2010 IEEE 12th International Symposium on High Assurance Systems Engineering, HASE 2010
Y2 - 3 November 2010 through 4 November 2010
ER -