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

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.