From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study

From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study

Miroslav Pajic∗, Zhihao Jiang†, Insup Lee†, Oleg Sokolsky† and Rahul Mangharam∗†

∗Department of Electrical and Systems Engineering University of Pennsylvania

abstract

Model-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. 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 ofverified 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.