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

M Pajic, Zhihao Jiang, I Lee, O Sokolsky, R Mangharam
April 2012
Cite Project Project DOI

Abstract

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.

Type
Conference paper
Publication
IEEE 18th Real Time and Embedded Technology and Applications Symposium
FormalMethod Pacemaker ModelChecking UPPAAL TimedAutomata
Zhihao Jiang
Zhihao Jiang
Assistant Professor

Zhihao Jiang is the director of Human-Cyber-Physical Systems Lab at ShanghaiTech University.

Related