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

Loading...
Thumbnail Image

Date

2014-01-01

Journal Title

Journal ISSN

Volume Title

Repository Usage Stats

221
views
255
downloads

Citation Stats

Abstract

Software-based control of life-critical embedded systems has become increasingly complex, and to a large extent has come to determine the safety of the human being. For example, implantable cardiac pacemakers have over 80,000 lines of code which are responsible for maintaining the heart within safe operating limits. As firmware-related recalls accounted for over 41% of the 600,000 devices recalled in the last decade, there is a need for rigorous model-driven design tools to generate verified code from verified software models. To this effect, we have developed the UPP2SF model-translation tool, which facilitates automatic conversion of verified models (in UPPAAL) to models that may be simulated and tested (in Simulink/Stateflow). We describe the translation rules that ensure correct model conversion, applicable to a large class of models. We demonstrate how UPP2SF is used in themodel-driven design of a pacemaker whosemodel is (a) designed and verified in UPPAAL (using timed automata), (b) automatically translated to Stateflow for simulation-based testing, and then (c) automatically generated into modular code for hardware-level integration testing of timing-related errors. In addition, we show how UPP2SF may be used for worst-case execution time estimation early in the design stage. Using UPP2SF, we demonstrate the value of integrated end-to-end modeling, verification, code-generation and testing process for complex software-controlled embedded systems. © 2014 ACM.

Department

Description

Provenance

Subjects

Citation

Published Version (Please cite this version)

10.1145/2584651

Publication Info

Pajic, M, Z Jiang, I Lee, O Sokolsky and R Mangharam (2014). Safety-critical medical device development using the UPP2SF model translation tool. Transactions on Embedded Computing Systems, 13(4 SPEC. ISSUE). 10.1145/2584651 Retrieved from https://hdl.handle.net/10161/11281.

This is constructed from limited available data and may be imprecise. To cite this article, please review & use the official citation provided by the journal.

Scholars@Duke

Pajic

Miroslav Pajic

Professor in the Department of Electrical and Computer Engineering

Miroslav Pajic's research focuses on design and analysis of cyber-physical systems with varying levels of autonomy and human interaction, at the intersection of (more traditional) areas of embedded systems, AI, learning and controls, formal methods and robotics.


Unless otherwise indicated, scholarly articles published by Duke faculty members are made available here with a CC-BY-NC (Creative Commons Attribution Non-Commercial) license, as enabled by the Duke Open Access Policy. If you wish to use the materials in ways not already permitted under CC-BY-NC, please consult the copyright owner. Other materials are made available here through the author’s grant of a non-exclusive license to make their work openly accessible.