=Paper=
{{Paper
|id=Vol-1531/paper9
|storemode=property
|title=Towards Integration of Modeling Methods for Cyber-Physical Systems
|pdfUrl=https://ceur-ws.org/Vol-1531/paper9.pdf
|volume=Vol-1531
|dblpUrl=https://dblp.org/rec/conf/models/Ruchkin15a
}}
==Towards Integration of Modeling Methods for Cyber-Physical Systems==
https://ceur-ws.org/Vol-1531/paper9.pdf
Towards Integration of Modeling Methods for
Cyber-Physical Systems
Ivan Ruchkin
Institute for Software Research
Carnegie Mellon University
Pittsburgh, PA 15213
iruchkin@cs.cmu.edu
Abstract—Safety-critical Cyber-Physical Systems (CPS) are CPS modeling and design methods [4]. As a result, safety-
growing increasingly more distributed, autonomous, and embed- critical CPS are prone to implicit errors that take a substantial
ded in our society. CPS engineering relies on modeling methods amount of time, effort, and funds to discover and fix. For
from different fields. Such methods are difficult to combine due
to their complexity and heterogeneity. Inconsistencies between example, in the General Motors ignition switch recall case it
models and analyses can lead to implicit design errors, which took years to discover an unexpected interaction between the
lead to critical CPS failures. Existing approaches to CPS model mechanical and electrical designs of the ignition switch that
integration fall short in terms of their flexibility, effectiveness, and lead to failures, loss of lives, and expensive recalls [5].
formal guarantees. To overcome these limitations and achieve
Some aspects of the integration problem have been suc-
better integration, I propose an integration approach based
on architectural views and analysis contracts. To enable my cessfully addressed in related research (see next section for
approach I develop a model-view consistency support framework, details). However, several important integration issues have
an analysis contracts framework, and a verification method for not yet been adequately addressed. One of them is the in-
multi-model integration properties. I claim that my approach is formality of relations between models and their integration-
feasible, more effective, and more cost-efficient than the existing
level representations (such as views). This relationship may
ones. I plan to validate my claims on realistic industrial academic
case studies of CPS modeling. be straightforward to establish and maintain for component-
based models such as Simulink1 and Verilog2 . However, some
I. P ROBLEM : M ODELING M ETHODS I NTEGRATION CPS models do not have syntactic support for component, or
their components are significantly different from the traditional
Modern software systems are growing increasingly more object-oriented modularization. For example, it is difficult
distributed, autonomous, and embedded in physical world. to componentize hybrid programs [6] which formally are
Such systems are important in science and technology because sequences of non-deterministic discrete jumps and continuous
they offer socioeconomic benefits beyond classic embedded evolutions. One way to deal with the absence of model
systems. For instance, self-driving cars promise dramatic re- structure is to rely on the engineer’s judgment and insight
ductions in the accident rate [1]. I will call systems with these to maintain the relationship to a view. However, this is effort-
characteristics Cyber-Physical Systems (CPS) because they intensive and error-prone.
are software-controlled and interact with complex physical Another aspect of the problem is that system designs un-
world, although other names such as autonomous robotics and dergo constant change. It is increasingly common to use auto-
mechatronics are often used to describe such systems as well. mated tools and algorithms to analyze models and derive their
Safety-critical CPS are difficult but important to engineer updated versions. I call such tools and algorithms analyses.
correctly. To tackle complex analog and digital processes, CPS Analyses are based on theories from specific engineering and
design and quality assurance rely on model-driven engineering scientific domains. For example, in the domain of processor
from various engineering fields, such as artificial intelligence, scheduling one finds thread-to-processor allocation via bin-
control theory, and mechatronics. This diversity of methods packing and processor frequency scaling [7] to derive an opti-
leads to complex and heterogeneous engineering processes that mal architecture of a real-time system. Some analyses change
are hard to combine for one system’s design. For example, at models: frequency scaling adjusts the frequency property of
least six distinct models of computation may need to co-exist processor components. For such analyses, it is impractical to
in a single system model [2]. re-establish consistency after every change: for every change
Ad hoc integration between diverse modeling methods may many global properties may need to be re-verified before
lead to miscommunication and inconsistencies, which turn another change is executed. Besides, analyses often make
into design errors and ultimately system failures [3]. I will implicit assumptions about the system or its environment, and
refer to such critical lack of integration as the Problem of it is important to verify these assumptions.
Modeling Methods Integration (MMI). Although partial solu-
tions to the MMI problem exist, CPS community has not yet 1 mathworks.com/products/simulink
developed general, effective, and practical ways to integrate 2 verilog.com
Finally, some multi-model consistency properties and an- with universal semantics that would hopefully serve as a lingua
alytic assumptions need to be expressed not only in terms franca of all CPS modeling methods. Such solutions often lead
of architectural elements (like components and connectors), to complex descriptions and an state space explosion, thus
but also in domain-specific terms that are not defined in not scaling properly for large systems. The second way is to
the architecture. Often such terms are too semantically low- preserve the diversity and heterogeneity of models through
level, and fully defining them in architectural views would be model integration. I will review several such frameworks in
impractical because one would have to “import” the full se- the remainder of this section.
mantics of the model, thus defeating the purpose of integration Software and systems engineering have a long heritage in
abstractions. As the next section describes, current integration compositional methods, some of which are being adapted to
approaches lack a way to express model-specific terms without CPS. One strand of research uses component contracts for
fully bringing the model semantics to the architectural level. composition [12]: each component has an interface with a
II. R ELATED W ORK formal contract. This approach works well for distributed
development of systems, but is often not appropriate for cross-
CPS engineering combines various modeling methods to cutting qualities like safety and security, since these qualities
address systemic properties like safety, stability, schedulability, would need to be propagated to almost every component in-
efficiency, security, and others. A modeling method is a cohe- terface, leading to scalability issues. Another way to compose
sive set of formalisms, algorithms, and processes to represent, system parts is by unifying components through their behavior
design, and analyze a system towards satisfaction of certain relations [13]. This is practical when behaviors are known and
properties. Much recent work on CPS modeling has focused can be easily specified, which, however, is not always the case
on formalisms and models. The related work can be split into for complex systems. My work takes the ideas of contract-
two categories: individual CPS modeling methods that I build based reasoning to a novel level of model-based analyses.
upon and try to incorporate into my approach, and CPS model
Ptolemy II [14] is an environment for simulation of diverse
integration approaches that can be seen as alternative solutions
models of computation like state machines, timed automata,
to the MMI problem.
and differential equations. Unfortunately, simulation does not
A. Modeling Methods for Cyber-Physical Systems provide strong theoretical guarantees like verification would,
Modeling methods for CPS differ depending on the scien- and not every CPS model has an explicit computation model.
tific field from which they originate. Since CPS engineering OpenMETA [15] is a platform based on formal logical se-
revolves around the boundary between discrete digital and mantic integration through metamodels. Despite its strong
continuous physical worlds, one of the most important charac- theoretical guarantees there is little guidance for models that
teristics of modeling methods is their treatment of potentially do not have explicit metamodels. Another limitation is that
continuous phenomena, such as time and space. At one end metamodel integration does not directly support verification
of this spectrum are classic software engineering models of changes to models. My research overcomes the limitations
like statecharts and process algebras [8]. These have support of these platforms.
for composability and automated verification. However, their A promising set of architectural approaches to the MMI
treatment of continuous phenomena is often too limited for problem focuses on choosing appropriate views for each CPS
CPS. formalism using annotated graphs as an underlying formalism
At the other end of the spectrum are models that include [16]. Flexibility of graph annotations enables customization for
continuities, like differential and difference equations [6] and each model and a variety of possible consistency verification
engineering tools like Simulink [9]. Although these models methods [17]. However, the architectural approach currently
are well-suited for traditional control settings, it is increas- has several limitations. First, model-view relations are infor-
ingly difficult to apply such models to complex autonomous mal and require substantial manual effort to create and update
systems. For instance, it is challenging to analyze behavioral throughout the engineering process. Another limitation is that
planning in signal-flow control models. The field of hybrid consistency is fragile due to frequent algorithmic changes to
systems aims to reconcile discrete and continuous system models. Finally, consistency properties have limited expres-
dynamics. A common model is a hybrid automaton [10] that siveness confined solely to the architectural level, incapable
combines continuous evolutions along differential equations of expressing richer properties.
with discrete state jumps. Although this field has enjoyed
success in symbolic and numeric computation for analysis of III. P ROPOSED S OLUTION : M ULTI -L EVEL
hybrid models, these models are notoriously complex, have A RCHITECTURAL AND A NALYTIC A PPROACH
limited scalability, and lack typical modularity mechanisms
[11], which makes them difficult to combine with common My research aims to improve the state-of-the-art in CPS
software and systems engineering methods. modeling method integration by employing a multi-level ap-
proach to the MMI problem. One abstraction is architectural
B. Integration Approaches views that represent model aspects that are relevant for inte-
Currently there are two major ways of addressing the MMI gration. The other level is the analysis level that considers
problem. One is to create a single language or formal system algorithms that change models and infer information from
them. Combining these two levels leads to a holistic and and update model-view relations have to be customized to the
effective treatment of CPS modeling integration issues. particular formalism in order to be effective. I take advantage
The overall scheme of my approach is shown in Fig. 1. of the flexibility of architectural styles – custom vocabularies
Consider two heterogeneous models to be integrated. The of architectural elements – to support customization and tailor
models are not completely independent, and there exists some transformation algorithms.
relationship between them (the cloud). However, this relation- Another function of the view level is establishing con-
ship is often too complex to express or verify directly. In- sistency between models through their views. This is done
stead, I create architectural view abstractions with integration- using consistency rules, which take form of constraints over
relevant information for each model. The views need to be multiple views and can be verified with constraint solving,
general enough to accommodate different formalisms and CPS for example SMT [7]. Properties that contain model-specific
application domains. terms (e.g., the current charge of a battery cell) require more
sophisticated verification methods such as model checking or
theorem proving.
B. Analysis Level
The analysis level automates sound execution of model-
based analyses, which depends on sound ordering and satis-
faction of assumptions and guarantees. To facilitate soundness
checking I designed the language of analysis contracts. Every
analysis is accompanied by its contract C that specifies inputs
I, outputs O, assumptions A, and guarantees G of the analysis,
in short C ≡ (I, O, A, G).
Sound analysis ordering is one where all analyses go in
order of their dependencies. For example, if analysis A1
depends on analysis A2 , then A2 should be executed before
A1 . A sound sequence of analyses is built by creating an anal-
ysis dependency graph and selecting any topological ordering
that ends with the desired analysis. The only exception for
this method is when there are cyclical dependencies, which
Fig. 1: The multi-level architectural and analytic approach. requires more sophisticated methods of dependency resolution.
To summarize, my approach promises more effective and
To support systematic change of models I introduce analyses less expensive CPS modeling method integration. The next
as part of the conceptual framework. Analyses read and change section presents preliminary evidence to supports that claim.
views, which propagate the changes to models. Analyses often IV. P RELIMINARY WORK
make assumptions that must be satisfied for the analysis to
be correct. For instance, frequency scaling is only applica- Here I describe two significant results: architectural views
ble if the system is deadline-monotonic [7]. If an analysis’ for hybrid programs and the analysis contracts framework.
assumptions are not satisfied, this analysis may produce an
A. Architectural View for Hybrid Programs
incorrect result, and therefore should not be executed. Since
some analyses modify the same set of views, input-output The hybrid program (HP) modeling and proving method,
dependencies arise and have to be properly resolved. based on hybrid programs and differential dynamic logic (dL)
[6], is particularly difficult to integrate with other modeling
A. View Level methods, in part due to HP expressiveness and lack of lan-
The view level is used to mediate complex interaction guage support for modularity. Each hybrid program contains
between analyses and models. A key to this mediation is fragments of various concerns that are highly intertwined
creating and maintaining two kinds of relations: view-view with each other, leading to poor modularity and possibility
and model-view. The former is more straightforward because of compositional errors [11].
views are specified in architecture description languages that To incorporate hybrid programs into my approach, I defined
have generally homogeneous structure of components and how architectural elements can be transformed into hybrid
connectors. Therefore this relationship can be maintained programs. That enabled high-level design and reasoning about
using a number of well-established techniques such as model HPs and at the same time eliminated manual effort of model-
transformation [18] or synchronization [19]. view consistency maintenance. A foundational abstraction
Model-view relations, on the other hand, require a more spe- for HP is an architectural view that contains actors HPA,
cial link between architectural descriptions and potentially less composers CPR, and connectors HPC . I defined an algorithm
structured models. I employ partial transformations and anno- to transform a view into a single HP via transformation
tations to overcome this problem. Mechanisms to establish functions of CPR and HPC . Given a view, it is possible to
reuse its parts and express its properties in dL, thus the level • Implementation of the property language for AADL in
of abstraction is elevated to components and systems from the OSATE2 architectural environment.
individual statements. I have also defined an analysis to check • A case study of integrating modeling methods in a
whether a view has a proper compositional structure, e.g., realistic industrial or academic CPS project.
whether an actor violates the laws of causality by manipulating Depending on the available time and resources, a number
variables of another actor outside existing connectors. of optional contributions can be made:
This work on architectural abstractions for hybrid programs, • A library of reusable CPS analyses, their contracts, and
implemented as a plugin to AcmeStudio [20], demonstrated view consistency rules;
feasibility and auxiliary benefits of automated support for • An instantiation of the model-view mechanism for an-
model-view relationships. other representative CPS formalism like mechanical 3D
CAD models or Simulink;
B. Analysis Contracts Framework • Theoretical analysis of the property specification method
This work investigated theoretical and practical aspects of in terms of its expressiveness and soundness.
using analysis contracts for integration [7]. Theoretical goals
VI. P LAN FOR T HESIS E VALUATION AND VALIDATION
were designing a syntax and semantics for contracts and creat-
ing algorithms that ensure sound execution of analyses. Prac- Below I make research claims about feasibility, correctness,
tical goals included application for existing domains beyond effectiveness, and generality of my approach to CPS modeling
the original thread scheduling and creation of an extensible method integration.
framework for analysis execution and contract verification. Feasibility: it is be possible to implement my approach in
To reach the theoretical goal I defined the syntax of anal- a tool environment that integrates CPS models. I.e., the tool
ysis contracts and described their semantics over verification should be capable of integrating representative CPS models
domains – collections of sets and functions that describe the and integration abstractions by specifying and verifying in-
essential elements of a technical domain. Towards the practical tegration consistency. I plan to validate feasibility by imple-
goal I designed and implemented the ACTIVE tool [21] 3 that menting the approach in a software tool.
supports execution of analyses in the OSATE2 architectural Correctness: verification procedures for the analysis con-
environment 4 for AADL. tracts and integration properties are sound. That requires
This research showed that analysis contracts are suitable demonstrating that the algorithms theoretically achieve their
for detection and prevention of integration errors in several goals of detecting and preventing inconsistencies in models.
domains: threads scheduling, battery scheduling [7], sensor Effectiveness: my approach semi-automatically detects and
trustworthiness, reliability, and control [22]. This work demon- prevents modeling method integration errors that would other-
strated the improvements in effectiveness and cost-efficiency wise be missed. I plan to validate effectiveness of the approach
in my approach to CPS modeling method integration. by applying it to collections of models for several systems and
showing that it can detect errors that would otherwise have not
V. E XPECTED CONTRIBUTIONS been made explicit.
Generality: my approach applies to a broad range of CPS
If successful, the proposed research will make the following modeling methods. I will validate this claim by demonstrating
contributions to the theory of model-driven engineering and the applicability of my approach to several representative CPS
cyber-physical systems: modeling methods.
• A formal description of the model-view consistency Since a significant part of this thesis research is applied, it is
mechanism and algorithms for its continuous update. critically important to evaluate these claims on practical cyber-
• A language for analysis contract specification and algo- physical systems and projects. Therefore, I plan to combine
rithms to support sound execution of analyses. These al- several validation methods. First, I check feasibility of my
gorithms include resolution of analytic data dependencies constructs and approach by implementing prototypes of sug-
and analysis contract verification. gested tools. I selected AcmeStudio and OSATE2 because the
• A language for expressing model-specific consistency former already served as a platform for multi-view CPS model
properties and analytic assumptions. consistency research [17], and the latter supports multiple
If successful, the proposed research will make the following architectural CPS analyses based on AADL. Second, I plan
contributions to the practice of model-driven engineering and to evaluate effectiveness and generality of my research on
cyber-physical systems: realistic industrial or academic projects (examples are below)
by taking them as case studies and applying my approach
• Implementation of the model-view formalism for Acme
to integrate modeling methods. In addition to the first two
in the AcmeStudio architectural environment.
approaches, I will use theoretical validation to investigate
• Implementation of the analysis contracts approach for
formal guarantees of my research in a form of theorems.
AADL in the OSATE2 architectural environment.
Finding appropriate CPS case studies can be challenging.
3 Available at github.com/bisc/active To simplify the search I establish the following criteria for the
4 wiki.sei.cmu.edu/aadl/index.php/Osate 2 desired case study projects:
• Heterogeneity: the project has at least two heterogeneous R EFERENCES
models or informal representations that are not integrated. [1] Paul Gao, Russel Hensley, and Andreas Zielke, “A road map to the
• Applicability: the system should have or have a possibility future for the auto industry,” McKinsey Quarterly, Oct. 2014.
of having discrepancies between models or representa- [2] P. Derler, E. A. Lee, and A. L. Sangiovanni-Vincentelli, “Addressing
Modeling Challenges in Cyber-Physical Systems,” University of Cali-
tions that would lead to critical design errors. fornia, Berkeley, Tech. Rep. UCB/EECS-2011-17, Mar. 2011.
• Realism: a project is intended for practical use in industry [3] J. Sztipanovits, X. Koutsoukos, G. Karsai, N. Kottenstette, P. Antsaklis,
or academia. V. Gupta, B. Goodwine, J. Baras, and S. Wang, “Toward a Science of
Cyber-Physical System Integration,” Proceedings of the IEEE, vol. 100,
• Scale: the project should involve at least three engineers. no. 1, pp. 29–44, Jan. 2012.
• Timing: the scope of the system can be adjusted so that [4] M. Wolf and E. Feron, “What Don’T We Know About CPS Ar-
validation does not take longer than one person-year. chitectures?” in Proceedings of the 52Nd Annual Design Automation
Conference, ser. DAC ’15. New York, NY, USA: ACM, 2015, pp.
Currently the candidate systems for conducting an integra- 80:1–80:4.
tion case study are: the NASA Europa spacecraft, 5 the Andy [5] Anton Valukas, “Report to Board of Directors of General Motors
Company Regarding Ignition Switch Recalls,” Jenner & Block, Tech.
Lunar Rover,6 the SMACCMPilot quadrotor, 7 the STARMAC Rep., May 2014.
quadrotor, 8 and the Toyota powertrain [23]. [6] A. Platzer, “Differential Dynamic Logic for Hybrid Systems,” Journal
of Automated Reasoning, vol. 41, no. 2, pp. 143–189, Aug. 2008.
VII. C URRENT S TATUS [7] I. Ruchkin, D. De Niz, S. Chaki, and D. Garlan, “Contract-based
Integration of Cyber-physical Analyses,” in Proceedings of the 14th
Most of the fundamental research towards my dissertation International Conference on Embedded Software, ser. EMSOFT ’14.
has been completed, but several theoretical and practical New York, NY, USA: ACM, 2014, pp. 23:1–23:10.
aspects remain. The tasks are summarized in Tab. I, with the [8] J. Magee and J. Kramer, Concurrency: State Models & Java Programs.
Wiley, Apr. 1999.
required work estimated to be completed in 11–16 months. [9] J. Dabney and T. L. Harman, Mastering SIMULINK 2. Upper Saddle
The next steps in my research focus on finalizing the design River, N.J.: Prentice Hall, 1998.
of the multi-model property language and conducting a case [10] R. Alur, T. A. Henzinger, and H. Wong-toi, “Symbolic Analysis of
Hybrid Systems,” 1997.
study of model integration. [11] I. Ruchkin, B. Schmerl, and D. Garlan, “Architectural Abstractions
for Hybrid Programs,” in Proceedings of the 18th International ACM
Task Completion Months left
SIGSOFT Symposium on Component-Based Software Engineering, ser.
Contract framework design 100% 0 CBSE ’15. New York, NY, USA: ACM, 2015, pp. 65–74.
Contract framework implementation 90% 0.5 [12] A. Sangiovanni-Vincentelli, W. Damm, and R. Passerone, “Taming Dr.
Model-view mechanism design 90% 0.5 Frankenstein: Contract-Based Design for Cyber-Physical Systems*,”
Model-view mechanism 75% 1 European Journal of Control, vol. 18, no. 3, pp. 217–238, 2012.
implementation [13] A. Rajhans, A. Bhave, I. Ruchkin, B. Krogh, D. Garlan, A. Platzer,
Multi-model property language design 50% 2-3 and B. Schmerl, “Supporting Heterogeneity in Cyber-Physical Systems
Multi-model property verification 50% 1 Architectures,” IEEE Transactions on Automatic Control, vol. 59, no. 12,
implementation pp. 3178–3193, Dec. 2014.
Case study search 50% 1-2 [14] C. Ptolemaeus, System Design, Modeling, and Simulation using Ptolemy
Case study execution 0% 2-4 Ii. Ptolemy.org, Sep. 2013.
Thesis writing 15% 2-3 [15] J. Sztipanovits, T. Bapty, S. Neema, L. Howard, and E. Jackson,
Thesis defense 0% 1 “OpenMETA: A Model and Component-Based Design Tool Chain for
(Optional) Theoretical evaluation of 0% 2 Cyber-Physical Systems,” in From Programs to Systems The Systems
model-view mechanism Perspective in Computing (FPS 2014). Grenoble, France: Springer,
(Optional) Another instantiation of 0% 1-2 Apr. 2014.
model-view mechanism [16] P. Fradet, D. Mtayer, and M. Prin, “Consistency Checking for Multiple
(Optional) Contract & property library 25% 1-2 View Software Architectures,” Software Engineering ESEC/FSE 99,
Total without optional 11-16 vol. 1687, pp. 410–428, 1999.
Total with optional 15-22 [17] A. Bhave, “Multi-View Consistency in Architectures for Cyber-Physical
Systems,” Ph.D. dissertation, Carnegie Mellon University, Dec. 2011.
TABLE I: Thesis tasks. [18] J. d. Lara and H. Vangheluwe, “AToM3: A Tool for Multi-formalism and
Meta-modelling,” in Proceedings of the 5th International Conference
on Fundamental Approaches to Software Engineering, ser. FASE ’02.
ACKNOWLEDGEMENTS London, UK, UK: Springer-Verlag, 2002, pp. 174–188.
[19] Istvn Rth, Andrs krs, and Dniel Varr, “Synchronization of abstract and
I thank my advisor David Garlan for his guidance and concrete syntax in domain-specific modeling languages,” Software and
support, and my collaborators Dionisio De Niz, Sagar Chaki, Systems Modeling, vol. 9, no. 4, pp. 453–471, 2010.
Bradley Schmerl, Ashwini Rao, and others for contributing to [20] B. Schmerl and D. Garlan, “AcmeStudio: Supporting Style-Centered
Architecture Development,” in Proceedings of the 26th International
this research. This work is supported by the National Science Conference on Software Engineering, ser. ICSE ’04. Washington, DC,
Foundation under Grant CNS-0834701, by the National Secu- USA: IEEE Computer Society, 2004, pp. 704–705.
rity Agency, and by the Department of Defense under Contract [21] I. Ruchkin, D. De Niz, S. Chaki, and D. Garlan, “ACTIVE: A Tool for
Integrating Analysis Contracts,” in The 5th Analytic Virtual Integration
No. FA8721-05-C-0003 with Carnegie Mellon University for of Cyber-Physical Systems Workshop, Rome, Italy, Dec. 2014.
the operation of the Software Engineering Institute, a federally [22] I. Ruchkin, A. Rao, D. De Niz, S. Chaki, and D. Garlan, “Eliminating
funded research and development center. Inter-Domain Vulnerabilities in Cyber-Physical Systems: An Analysis
Contracts Approach,” 2015, submitted for publication.
5 nasa.gov/europa [23] X. Jin, J. V. Deshmukh, J. Kapinski, K. Ueda, and K. Butts, “Powertrain
6 lunar.cs.cmu.edu Control Verification Benchmark,” in Proceedings of the 17th Interna-
7 smaccmpilot.org tional Conference on Hybrid Systems: Computation and Control, ser.
8 hybrid.eecs.berkeley.edu/starmac
HSCC ’14. New York, NY, USA: ACM, 2014, pp. 253–262.