| 606 |
@PhdThesis{Ruchkin:2019:Thesis,
AUTHOR = {Ruchkin, Ivan},
TITLE = {Integration of Modeling Methods for Cyber-Physical Systems},
YEAR = {2019},
MONTH = {March},
SCHOOL = {Carnegie Mellon University},
PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/ruchkin-20190328-final.pdf},
ABSTRACT = {Cyber-physical systems (CPS) incorporate digital (cyber) and mechanical (physical)
elements that interact in complex ways. Many safety-critical CPS, such as
autonomous vehicles and drones, are becoming increasingly widespread and hence
demand rigorous quality assurance. To this end, CPS engineering relies on modeling
methods, which use models to represent the system and design-time analyses to
interpret/change the models. Coming from diverse scientific and engineering fields,
these modeling methods are difficult to combine, or integrate, due to implicit relations
and dependencies between them. CPS failures can lead to substantial damage or
loss of life, and are often due to two key integration challenges: (i) inconsistencies
between models — contradictions in models that do not add up to a cohesive design,
and (ii) incorrect interactions of analyses — analyses performed out-of-order and in
mismatched contexts, leading to erroneous analysis outputs.
This thesis presents a novel approach to detect and prevent integration issues
between CPS modeling methods during the design phase. To detect inconsistencies
between models, the approach allows engineers to specify integration properties
— quantified logical statements that relate elements of multiple models — in the
Integration Property Language (IPL). IPL statements describe verifiable conditions
that are equivalent to an absence of inconsistencies. To interface with the models,
IPL relies on integration abstractions — simplified representations of models
for integration purposes. This thesis proposes two abstractions: views (annotated
component-and-connector models, inspired by software architecture) and behavioral
properties (expressions in model-specific property languages, such as the linear temporal
logic). Combining these abstractions lets engineers relate model structure and
behavior in IPL statements. To ensure correct interactions of analyses, I introduce
analysis contracts — a lightweight specification that captures inputs, outputs, assumptions,
and guarantees for each analysis, in terms of the integration abstractions.
Given these contracts, an analysis execution platform performs analyses in the order
of their dependencies, and only in the contexts that guarantee correct outputs.
My approach to integration was validated on four case studies of CPS modeling
methods in different systems: energy-aware planning in a mobile robot, collision
avoidance in a mobile robot, thread/battery scheduling in a quadrotor, and reliable/
secure sensing in an autonomous vehicle. This validation has shown that the
approach can find safety-critical errors by specifying expressive integration properties
and soundly checking them within practical constraints — all while being
customizable to heterogeneous models, analyses, and domains.},
NOTE = {Institute for Software Research Technical Report CMU-ISR-18-107},
KEYWORDS = {Cyberphysical Systems, Formal Methods}
}
|
|
