Show simple item record

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

dc.contributor.author Jiang, Z
dc.contributor.author Lee, Insup
dc.contributor.author Mangharam, R
dc.contributor.author Pajic, M
dc.contributor.author Sokolsky, O
dc.date.accessioned 2015-12-29T02:08:19Z
dc.date.issued 2014-01-01
dc.identifier.issn 1539-9087
dc.identifier.uri http://hdl.handle.net/10161/11281
dc.description.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.
dc.relation.ispartof Transactions on Embedded Computing Systems
dc.relation.isversionof 10.1145/2584651
dc.title Safety-critical medical device development using the UPP2SF model translation tool
dc.type Journal article
pubs.issue 4 SPEC. ISSUE
pubs.organisational-group Computer Science
pubs.organisational-group Duke
pubs.organisational-group Electrical and Computer Engineering
pubs.organisational-group Pratt School of Engineering
pubs.organisational-group Trinity College of Arts & Sciences
pubs.publication-status Published
pubs.volume 13
dc.identifier.eissn 1558-3465


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record