Safety-critical medical device development using the UPP2SF model translation tool

Abstract

This paper presents UPP2SF, a model-translation tool for turning verified UPPAAL models into Simulink/Stateflow models that can be simulated, tested, and compiled into code. Through a pacemaker case study, it demonstrates correct model conversion, support for timing analysis, and an end-to-end workflow from verification to hardware-level testing.