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

摘要: Model-Driven Design (MDD) of cyber-physical systems advocates for design procedures that start with formal modeling the real-time system, followed by model's verification at an early stage. The verified model must then be translated to a more detailed simulation-based testing and finally into executable code in physical implementation. As later stages build on same core model, it is essential models used earlier pipeline are valid approximations developed downstream. focus this effort development translation tool, UPP2SF, how integrates system modeling, verification, model-based WCET analysis, simulation, generation MDD based framework. UPP2SF facilitates automatic conversion timed automata-based (in UPPAAL) may simulated tested Simulink/State flow). We describe rules ensure correct, efficient applicable large class models. show tool enables implantable cardiac pacemaker. demonstrate preserves behaviors pacemaker from UPPAAL State flow. resultant flow chart automatically converted C hardware platform set requirements.