Name
Title | ||
|---|---|---|
Linking abstract analysis to concrete design: A hierarchical approach to verify medical CPS safety |
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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1109/ICCPS.2014.6843718 | Cyber-Physical Systems |
Keywords | Field | DocType |
formal specification,formal verification,medical computing,safety,abstract component specification,associated tools,complex cyber-physical system model,concrete component description,concrete design,design complexity management,formal reasoning,hierarchical approach,linking abstract analysis,medical CPS safety,medical device cyber-physical system,multiple abstraction layers,multiple modeling formalisms,system properties,verification paradigms,verification tractability,Medical CPS,Model-based development,Verification | Functional verification,Intelligent verification,Computer science,Model-based design,Runtime verification,Verification,Theoretical computer science,High-level verification,Abstraction layer,Rotation formalisms in three dimensions | Conference |
ISSN | Citations | PageRank |
2375-8317 | 4 | 0.45 |
References | Authors | |
15 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Murugesan, A. | 1 | 13 | 1.04 |
| Sokolsky, O. | 2 | 6 | 0.79 |
| Rayadurgam, S. | 3 | 4 | 0.45 |
| Michael W. Whalen | 4 | 1096 | 70.54 |