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

摘要

This paper presents UPP2SF, a model-translation tool that links formally verified UPPAAL models to Simulink/Stateflow models for simulation, code generation, and testing. A pacemaker case study shows how the approach preserves behavior across the toolchain and supports model-driven development of real-time cyber-physical systems.