Linking abstract analysis to concrete design: A hierarchical approach to verify medical CPS safety

Anitha Murugesan, Oleg Sokolsky, Sanjai Rayadurgam, Michael Whalen, Mats Heimdahl, Insup Lee

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Scopus citations

Abstract

To manage design complexity and provide verification tractability, models of complex cyber-physical systems are typically hierarchically organized into multiple abstraction layers. Formal reasoning about such systems, therefore, usually involves multiple modeling formalisms, verification paradigms, and associated tools. System properties verified using an abstract component specification in one paradigm must be shown to logically follow from properties verified - possibly using a different paradigm - on a more concrete component description. As component specifications at one layer of abstraction get elaborated into more concrete component descriptions at the next lower level, abstraction induced differences come to the fore; differences that have to be reconciled. In this paper, we present an approach to tie together distinct verification paradigms and reconcile these abstraction induced differences using a medical device cyber-physical system as an example. While the specifics are particular to the example at hand, we believe the techniques are applicable in similar situations for verifying cyber-physical system properties.

Original languageEnglish (US)
Title of host publication2014 ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2014
PublisherIEEE Computer Society
Pages139-150
Number of pages12
ISBN (Print)9781479949311
DOIs
StatePublished - 2014
Event5th IEEE/ACM International Conference on Cyber-Physical Systems, ICCPS 2014 - Berlin, Germany
Duration: Apr 14 2014Apr 17 2014

Publication series

Name2014 ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2014

Other

Other5th IEEE/ACM International Conference on Cyber-Physical Systems, ICCPS 2014
CountryGermany
CityBerlin
Period4/14/144/17/14

Keywords

  • Medical CPS
  • Model-based development
  • Verification

Fingerprint Dive into the research topics of 'Linking abstract analysis to concrete design: A hierarchical approach to verify medical CPS safety'. Together they form a unique fingerprint.

Cite this