Skip to main content
Duke University Libraries
DukeSpace Scholarship by Duke Authors
  • Login
  • Ask
  • Menu
  • Login
  • Ask a Librarian
  • Search & Find
  • Using the Library
  • Research Support
  • Course Support
  • Libraries
  • About
View Item 
  •   DukeSpace
  • Duke Scholarly Works
  • Scholarly Articles
  • View Item
  •   DukeSpace
  • Duke Scholarly Works
  • Scholarly Articles
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

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

Thumbnail
View / Download
2.6 Mb
Date
2014-01-01
Authors
Pajic, M
Jiang, Z
Lee, I
Sokolsky, O
Mangharam, R
Repository Usage Stats
221
views
248
downloads
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.
Type
Journal article
Permalink
https://hdl.handle.net/10161/11281
Published Version (Please cite this version)
10.1145/2584651
Publication Info
Pajic, M; Jiang, Z; Lee, I; Sokolsky, O; & Mangharam, R (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.
Collections
  • Scholarly Articles
More Info
Show full item record

Scholars@Duke

Pajic

Miroslav Pajic

Dickinson Family Associate Professor
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.
Open Access

Articles written by Duke faculty are made available through the campus open access policy. For more information see: Duke Open Access Policy

Rights for Collection: Scholarly Articles


Works are deposited here by their authors, and represent their research and opinions, not that of Duke University. Some materials and descriptions may include offensive content. More info

Make Your Work Available Here

How to Deposit

Browse

All of DukeSpaceCommunities & CollectionsAuthorsTitlesTypesBy Issue DateDepartmentsAffiliations of Duke Author(s)SubjectsBy Submit DateThis CollectionAuthorsTitlesTypesBy Issue DateDepartmentsAffiliations of Duke Author(s)SubjectsBy Submit Date

My Account

LoginRegister

Statistics

View Usage Statistics
Duke University Libraries

Contact Us

411 Chapel Drive
Durham, NC 27708
(919) 660-5870
Perkins Library Service Desk

Digital Repositories at Duke

  • Report a problem with the repositories
  • About digital repositories at Duke
  • Accessibility Policy
  • Deaccession and DMCA Takedown Policy

TwitterFacebookYouTubeFlickrInstagramBlogs

Sign Up for Our Newsletter
  • Re-use & Attribution / Privacy
  • Harmful Language Statement
  • Support the Libraries
Duke University