TY - GEN
T1 - Linking abstract analysis to concrete design
T2 - 5th IEEE/ACM International Conference on Cyber-Physical Systems, ICCPS 2014
AU - Murugesan, Anitha
AU - Sokolsky, Oleg
AU - Rayadurgam, Sanjai
AU - Whalen, Michael
AU - Heimdahl, Mats
AU - Lee, Insup
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
KW - Medical CPS
KW - Model-based development
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=84904464667&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84904464667&partnerID=8YFLogxK
U2 - 10.1109/ICCPS.2014.6843718
DO - 10.1109/ICCPS.2014.6843718
M3 - Conference contribution
AN - SCOPUS:84904464667
SN - 9781479949311
T3 - 2014 ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2014
SP - 139
EP - 150
BT - 2014 ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2014
PB - IEEE Computer Society
Y2 - 14 April 2014 through 17 April 2014
ER -