From Verification to Implementation: A Model Translation Tool and a Pacemaker Case StudyProceedings of the 18th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2012)
Document TypeConference Paper
Date of this Version1-1-2012
AbstractModel-Driven Design (MDD) of cyber-physical systems advocates for design procedures that start with formal modeling of the real-time system, followed by the model’s verification at an early stage. The verified model must then be translated to a more detailed model for simulation-based testing and finally translated into executable code in a physical implementation. As later stages build on the same core model, it is essential that models used earlier in the pipeline are valid approximations of the more detailed models developed downstream. The focus of this effort is on the design and development of a model translation tool, UPP2SF, and how it integrates system modeling, verification, model-based WCET analysis, simulation, code generation and testing into an MDD based framework. UPP2SF facilitates automatic conversion of verified timed automata-based models (in UPPAAL) to models that may be simulated and tested (in Simulink/Stateflow). We describe the design rules to ensure the conversion is correct, efficient and applicable to a large class of models. We show how the tool enables MDD of an implantable cardiac pacemaker. We demonstrate that UPP2SF preserves behaviors of the pacemaker model from UPPAAL to Stateflow. The resultant Stateflow chart is automatically converted into C and tested on a hardware platform for a set of requirements.
Copyright/Permission Statement© 2012 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
- Model-based development,
- model translation,
- medical devices,
- validation & verification,
- real-time systems
Citation InformationMiroslav Pajic, Zhihao Jiang, Insup Lee, Oleg Sokolsky, et al.. "From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study" Proceedings of the 18th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2012) (2012) p. 173 - 184
Available at: http://works.bepress.com/rahul_mangharam/32/