Architectural and Analytic Integration of Cyber-Physical System Models Ivan Ruchkin Institute for Software Research Carnegie Mellon University Pittsburgh, PA 15213 iruchkin@cs.cmu.edu Abstract—Modeling methods for Cyber-Physical Systems CPS modeling and design methods [5]. As a result, safety- (CPS) originate in various engineering fields, and are difficult to critical CPS are prone to implicit errors that take a substantial use together due to their heterogeneity. Inconsistencies between amount of time, effort, and funds to discover and fix. For mutually oblivious models and analyses often lead to implicit de- sign errors, which may cause catastrophic failures of critical CPS. example, the GM ignition switch recall was caused by an Such consistency issues are not fully solved by the state-of-the-art unexpected interaction between the mechanical and electrical integration methods, which lack generality, formal guarantees, designs of the ignition switch, leading to failures, loss of lives, and effectiveness. To overcome these limitations and achieve and expensive recalls [6]. better integration, this paper outlines a two-level integration approach based on architectural views and analysis contracts. One of the approaches to the MMI problem focuses on In particular, this paper proposes languages and algorithms choosing an appropriate component abstraction (a“view”) for to specify and verify important integration properties, such as each CPS formalism, using annotated graphs as an underlying correct analysis execution and rich consistency of architectural notation [7]. This approach takes advantage of flexibility of views. According to the results to date, this approach shows graph annotations to support custom models and a variety of promise in detection and prevention of implicit errors, which would be difficult to fix otherwise. consistency verification methods. Despite its advantages, the architectural approach currently has several significant lim- I. I NTRODUCTION itations. First, model-view relations are informal and require Modern software systems are growing more distributed, au- substantial manual effort to be created and updated throughout tonomous, and embedded in physical world [1]. Such systems the engineering process. Another limitation is that consistency are increasingly important because they offer socioeconomic is fragile due to frequent algorithmic changes to models (we benefits beyond classic embedded systems. For example, fully call these algorithms analyses). Finally, consistency properties automated self-driving cars promise dramatic reductions in have limited expressiveness confined solely to the architectural the accident rate [2]. Such systems are often called Cyber- level, incapable of expressing richer properties. Physical Systems (CPS)1 because they are combine software This paper introduces the two-level integration approach with complex physical dynamics. that overcomes the above limitations. One level of abstraction Safety-critical CPS are difficult but important to engineer is the architectural view level that represents the aspects of correctly. To tackle complex analog and digital processes, CPS each model that are relevant for integration. The other level design and quality assurance rely on model-driven engineering is the analysis level that focuses on algorithms that change from various scientific and engineering fields, such as artificial models and infer information from them. Combining these two intelligence, control theory, and mechanical design. This diver- levels leads to a holistic treatment of CPS modeling integration sity of methods leads to complex and heterogeneous models issues. In particular, this research makes the following major that are hard to combine for one system’s design. For example, contributions to the field of cyber-physical systems: at least six distinct models of computation may need to co- A Formalization of, and automated support for, CPS model- exist in a single system model [3]. view relations – a formalism and algorithms for auto- Failure to combine multidisciplinary modeling methods mated creation and updating of model-view relations, properly may lead to miscommunication and inconsistencies, even for models that are not structured based on com- which turn into design errors and ultimately system failures ponents, e.g., hybrid programs [8]. Preliminary work [4]. In this paper, such issues are generally called the Problem (Sec. V) shows that automation of model-view relations of Modeling Methods Integration (MMI) – absence of integra- is feasible and provides auxiliary modeling benefits, such tion leading to erroneous designs. Although partial solutions as component-based analysis and reuse of models. to the MMI problem exist, CPS community has not yet B A framework for automated analysis-driven change in developed general, effective, and practical ways to integrate CPS models – a language for specifying analysis de- 1 Such systems are also sometimes referred to as autonomous robotics and pendencies with formal contracts, and an algorithm for mechatronics. sound ordering and execution of analyses. Preliminary work shows that this framework prevents modeling errors challenging to analyze behavioral planning, which in important that occur due to incorrect ordering of analysis execution. to CPS, in signal-flow control models. C A method for domain-specific specification and verifica- The field of hybrid systems aims to combine discrete and tion of CPS model consistency and analytic soundness – continuous system dynamics. A common model is a hybrid au- a language to express model-specific CPS properties, and tomaton [13] that combines continuous differential equations an algorithm to verify such properties. This language in- with discrete state jumps. Although hybrid systems have en- corporates model-specific terms beyond the architectural joyed success in symbolic and numeric analysis, hybrid models level, and can used in Contributions A and B. Preliminary are notoriously complex and have limited scalability, and thus work demonstrates that this language can detect integra- have to be applied selectively in practice. Another limitation is tion errors that would not have been detectable purely at that hybrid models lack typical modularity mechanisms [14], the level of architectural views. and hence are difficult to combine with common models in All three elements of the approach will be implemented software and systems engineering. in popular architecture modeling languages and environments, B. Integration Approaches and validated on realistic academic and industrial case studies to show effectiveness and generality of the approach. Currently there are two major ways of addressing the MMI Next section gives more background on CPS modeling problem. One is to create a single language or formal system methods and existing work that addresses the MMI problem. with universal semantics that would hopefully serve as a lingua Sec. III contains more detail on the MMI problem, and Sec. IV franca of all CPS modeling methods. Such solutions often presents the two-level approach to MMI. The last section lead to very complex descriptions and quick explosion of state discusses research completed to date and concludes the paper. space [15], thus becoming inapplicable to large systems. The second way is to preserve the diversity and heterogeneity of II. BACKGROUND AND R ELATED W ORK models through model integration. The rest of this section A modeling method is a cohesive set of formalisms, algo- reviews several such frameworks. rithms, and processes to represent, design, and analyze a sys- Software and systems engineering have a significant her- tem towards satisfaction of certain properties. CPS engineering itage in compositional methods, some of which have been combines various modeling methods to address systemic prop- adapted to CPS. One strand of research composes components erties like safety, stability, schedulability, security, and others. using contracts [16]: each component has an interface with The work related to this research can be split into two a formal contract. This approach works well for distributed categories: individual CPS modeling methods that can be sup- development of systems, but is often inappropriate for cross- ported by an integration approach, and CPS model integration cutting qualities like safety and security. Another way to approaches that can be seen as alternative solutions to the MMI compose system parts is by unifying components through their problem. behavior relations [17]. This is practical when behaviors are known and easily specified, which, however, is not always the A. Modeling Methods for Cyber-Physical Systems case for complex systems. The work in this paper uses well- Modeling methods for CPS differ depending on a scientific known contract-based reasoning at a novel level of analyses. field where they originate. Since CPS engineering revolves Ptolemy II [18] is a platform for rich simulation of diverse around the boundary between discrete digital and continuous models of computation. It can be used to co-simulate het- physical worlds, one of the most important characteristics of erogeneous models like state machines, Petri nets, and timed modeling methods is their treatment of potentially continuous automata. Although this is a promising integration method for phenomena, such as time and space. On the one hand of hands-on engineering, it does not provide strong theoretical this spectrum are classic software engineering models like guarantees (like those behind formal verification). Another statecharts and process algebras [9]. These models are easier to obstacle is that not every CPS model has a well-defined compose and verify using such techniques as model checking. computation model: some models are more declarative than However, their treatment of continuous quantities is very imperative, for example logical and functional models. The limited and not satisfactory for CPS [10] A special place two-level integration approach incorporates modeling meth- among discrete formalisms is taken by architectural models ods and verification regardless of how definable models of such as UML, SysML, and AADL [11]. These models include computation are. flexible elements such as profiles, types, and annexes to allow Another approach to the MMI problem is based on logical specialization and extension, making architectural models par- integration through metamodels and formal semantics, such ticularly suitable to be a foundation of CPS integration. as in OpenMETA and CyPhyML [19]. This method provides On the other hand of the spectrum are classic control models strong theoretical guarantees and practical engineering support written in differential or difference equations [8] and their when a metamodel is known. However, there is little guidance engineering counterparts like Simulink [12]. Although these for models that do not have explicit metamodels, or whose models are well-suited for traditional control settings like metamodels are too computationally complex and only partial physical process control, it is increasingly difficult to apply integration is possible. Another limitation is that metamodel such models to complex intelligent systems. For instance, it is integration does not directly support verification of changes to models. Our research, on the other hand, does not depend on analyses change models locally, it is impractical to maintain explicit metamodels and provides structured change support consistency in a traditional way: for every local change, many that can augment metamodel integration. global properties may need to be re-verified before another Prior work on architecture-based CPS model consistency local change can be made. Besides, analyses often make defined a vocabulary of CPS terms, and used it to check struc- implicit assumptions about the system and its environment, tural consistency [20]. It however does not address the question and it’s important to verify these assumptions – otherwise of how model-view relations are created and maintained, analytic results may be incorrect. leaving it to error-prone and expensive manual effort. Prior Finally, some model consistency properties and analytic work on analysis contracts offers limited, bounded verification assumptions need to be expressed not only in terms of ar- with Alloy and focuses on openness of runtime models [21]. chitectural elements (components and connectors), but also in In contrast, our work on analysis contracts advances that domain- and model-specific terms (e.g., current battery cell state of the art through an extensible contracts language with charge [25]) that are not defined in architectural models. Often theoretically defined semantics and verification mechanisms. such terms are too semantically low-level, and fully defining them in architectural views would be impractical because one III. P ROBLEM : M ODELING M ETHOD I NTEGRATION would have to “import” the full detailed semantics of a model, As mentioned in Sec. I, the Modeling Method Integration thus defeating the purpose of integration abstractions. (MMI) problem is caused by a critical lack of integration To clarify the expressiveness issue, consider an assump- between CPS modeling methods that leads to design errors and tion of the frequency scaling analysis – behavioral deadline- ensuing substantial operational losses. Consider for example monotonicity of threads on each processor [25]. That is, if a a self-driving car that autonomously navigates through an thread preempts another, it should have a smaller deadline. To urban environment, supported by intelligent infrastructure, express this statement logically, in addition to the architectural such as smart traffic signals [22]. All aspects of the car concepts (threads, processors, bindings, and deadlines) we design – electrical, mechanical, thermal, power, control, and refer to the non-architectural concept of thread preemption. communication – need to be properly aligned and, ideally, In this case, preemption is modelled as a logical predicate verified before manufacturing in order to ensure safety and CanPrmpt over a pair of threads that holds iff the first acceptable performance of the system. If modeling methods thread preempts the second at the (implicitly modeled) current that address these aspects invalidate each other, it is likely moment of time. Then the assumption can be written as: that difficult-to-find discrepancies would be introduced into the design. ∀t1 , t2 ∈ T · t1 6= t2 ∧ CPUBind(t1 ) = CPUBind(t2 ) : Some parts of the MMI problem have been successfully (1) addressed in related research. For example, architectural in- G (CanPrmpt(t1 , t2 ) =⇒ Dline(t1 ) < Dline(t2 )), tegration abstractions have been used to represent model where T is the set of all threads in the system; CPUBind(t) structure and behavior, check consistency, and compose in- is the processor that thread t executes on; G (P ) is a global dependent components [23]. Model integration properties can modality in linear temporal logic (LTL) [26] requiring that be expressed as parametric constraints over sets of views [24]. predicate P holds at all times; and Dline(t) is the offline However, several important integration issues have not been deadline of thread t. We need to systematically and scalably resolved. One of them is the informality of relations between interpret and verify statements like the above, and the existing heterogeneous models and their integration-level represen- frameworks fall short of doing so. tations (such as views). These relations may be easier to establish and maintain for component-based models, such as A. Challenges Simulink and Verilog. However, some CPS models do not have native support for components. For example, hybrid programs The MMI problem can be encountered in a variety of are difficult to componentize [8] because they formally are engineering settings outside of CPS. For example, traditional sequences of potentially non-deterministic discrete jumps and software engineering uses several notations and reasoning continuous evolutions. Traditionally, such fuzzy model-view styles, and sometimes their interoperability is required [27]. relations are handled by an engineer’s judgment and insight, It is however in the CPS context that this problem becomes which is an effort-intensive and error-prone way. particularly challenging due to several reasons: Another aspect of the MMI problem is that system designs • No single discipline in CPS owns a full solution. Het- undergo constant change. It is increasingly common to use erogeneous methods need to, as least partially, reconcile automated tools and algorithms to analyze and augment mod- conflicting paradigms to achieve practical integration. els. We call such tools and algorithms analyses. Analyses are • Correct integration often depends upon satisfaction of based on theories and methods from diverse engineering and implicit assumptions. Many engineers do not challenge scientific domains. For example, in the domain of real-time the assumptions of their discipline, and aren’t aware of processor scheduling, thread-to-processor allocation via bin- the assumptions in other disciplines. Discovering such packing and processor frequency scaling [25] are analyses that assumptions and their violations is therefore a difficult derive a more optimal architecture of a real-time system. If task with unpredictable outcomes. • Usually models and source code of safety-critical CPS with components, connectors, and properties that are defined in cannot be found on popular collaborative websites such a particular architectural style – a custom vocabulary of archi- as GitHub. Conducting an evaluative case study of inte- tectural elements. Using views for integration requires creating gration methods requires overcoming organizational and and maintaining two kinds of relations: view-view and model- legal barriers to access protected systems. view. The former is more straightforward because views are Nevertheless, it is possible to improve CPS modeling specified in ADLs that have generally homogeneous structure method integration. The next section presents a two-level of components and connectors. Therefore this relationship can approach to the MMI problem. be maintained using a number of well-established techniques such as model transformation [28] or synchronization [29]. IV. A PPROACH : A RCHITECTURAL AND Model-view relations, on the other hand, require a more A NALYTIC I NTEGRATION special link between views and potentially less structured The overall scheme of the two-level integration approach models. A view needs to abstract out some semantics and is shown in Fig. 1. Consider two heterogeneous models to be structure of a model. We use view-model mappings and integrated. The models are not completely independent, and transformations to automatically support model-view relations. there exists some relationship between them. This relationship These mappings and transformations have to be customized to is however too complex to express or verify directly. Instead, the particular formalism in order to be effective. The approach we create architectural view abstractions with integration- takes advantage of the flexibility of architectural styles to relevant information for each model. The views need to be support customization and tailor transformation algorithms. general enough to accommodate different formalisms (e.g., For instance, the hybrid program view [14] describes which hybrid programs or Simulink) and CPS application domains component “owns” how each hybrid program variable. (e.g., avionics or transportation). Another function of the view level is establishing consis- To support systematic change of models, analyses are con- tency between models through their views. That is done by sidered first-class entities. Analyses read and change views, specifying and verifying consistency rules, which take form which propagate the changes to models. Analyses often have of constraints over multiple views and can be verified with their applicability limited by assumptions. If an analysis’ constraint solving [30]. Properties that contain model-specific assumptions are not satisfied, this analysis may produce an terms like CanPrmpt (see Eq. 1) require more sophisticated incorrect result should not be executed. Some analyses have verification methods, such as model checking or theorem guarantees – statements that should hold after an analysis is proving. executed. If this is not the case, the changes made by this B. Analysis Level analysis should be rolled back. Since some analyses modify the same set of views, input-output dependencies arise and The analysis level automates sound execution of model- have to be resolved. based analyses, which depends on correct ordering and satis- faction of assumptions and guarantees. The language of anal- ysis contracts facilitates soundness checking. 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). Correct analysis ordering is one where all analyses go in or- der of their dependencies. For example, if analysis A1 depends on analysis A2 2 , then A2 should be executed before A1 . For instance, a CPU scheduling analysis, which determines the voltage required by CPUs, should be followed by a battery design analysis, which uses the voltage as a requirement. A sound sequence of analyses is built by creating an analysis 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 requires more sophisticated methods of dependency resolution. Assumption and guarantee verification is done in the same way as consistency property verification on the view level. The two-level integration approach demonstrated in Fig. 1 Fig. 1. Architectural and analytic approach to CPS model integration. has the following advantages: • By combining architectural and analytic perspectives, it A. View Level incorporates a large body of prior work and offers diverse opportunities to integrate modeling methods. The view level is used to mediate complex interaction be- tween analyses and models. An view is an architectural model 2 That is, one of A 2 outputs is one of A1 inputs. • Important but subtle integration properties that span mul- This work on architectural abstractions for hybrid programs tiple domains and formalisms can now be expressed and towards Contribution A, implemented as a plugin to AcmeS- verified at an appropriate abstraction level, thanks to tudio [31], demonstrated feasibility of automated maintenance Contribution C. of model-view relationship. It opens future research directions • The bottom-up philosophy behind the approach enables in construction of integration tools and investigation of theo- adding new modeling methods without up-front planning, retical soundness for HP view analyses. in contrast with existing top-down approaches that are dependent on specific formalisms. B. Analysis Contracts Framework The approach also has several limitations: This work investigated theoretical and practical aspects of • It may be difficult to provide integration for incomplete using analysis contracts for integration (towards Contribu- and informal models, which often require unique formal- tion B) [25]. Theoretical goals were designing the syntax izations and algorithms. and semantics for contracts and devising algorithms that • The scalability of formal verification techniques depends ensure sound execution of analyses. Practical goals included on carefully designed abstractions and high-quality tools, formalization of existing domains beyond the original one which may not always be available. (thread scheduling) and creation of an extensible framework • It may be impractical to invest into an up-front formal for analysis execution and contract verification. integration of views and analyses in CPS projects that do Towards the theoretical goals, analysis contracts as quadru- not use many heterogeneous modeling methods. ples C (see Sec. IV above for details). Their semantics is To summarize, the two-level approach is promising to make described over verification domains – collections of sets and CPS modeling method integration more effective and less functions that describe the essential elements of a technical effortful. The next section presents preliminary evidence that domain. Towards the practical goal, the ACTIVE tool [32] was supports this claim. designed and implemented3 to support correct execution of V. R ESULTS TO DATE analyses in an AADL environment OSATE2 [33]. This research showed that analysis contracts are suitable This section describes two significant results: architectural for detection and prevention of integration errors in several views for hybrid programs and the analysis contracts frame- domains: threads scheduling, battery scheduling [25], sensor work. trustworthiness, reliability, and control [34]. This work demon- A. Architectural Views for Hybrid Programs strated the improvements in effectiveness and cost-efficiency The hybrid program modeling method, based on hybrid in CPS modeling method integration. programs (HP) and differential dynamic logic (dL) [8], is This paper outlined the two-level integration approach for particularly difficult to integrate with other modeling methods, CPS modeling methods. The next steps in this research are in part due to HP expressiveness and lack of support for mod- finalizing the design of the integration property language (Con- ularity. Each hybrid program contains fragments of various tribution C), and conducting case studies of model integration concerns, from the physical environment of the system to the in realistic academic and industrial cyber-physical systems, type of sensing and actuation. These fragments are highly such as NASA Europa Orbiter 4 and Carnegie Mellon Andy intertwined with each other across many statements of the Rover 5 . Candidates for case studies would be systems with program. Specification of interacting components, e.g., a robot diverse modeling and analytic artifacts that can be used to and an obstacle, is also dispersed through the body of a HP. validate effectiveness and generality of the approach. Leading to poor HP modularity, these issues inspired work on creating an architectural abstraction of hybrid programs [14]. ACKNOWLEDGEMENTS To incorporate hybrid programs into the approach, we I thank my advisor David Garlan for his guidance and defined an architectural HP view, which defines how archi- support. I thank Dionisio De Niz, Sagar Chaki, Bradley tectural elements are transformed into hybrid programs. That Schmerl, Ashwini Rao, and other collaborators for contributing enabled high-level design and reasoning about HPs and at the to this research. I am also grateful to anonymous reviewers for same time eliminated manual effort of model-view consistency their helpful comments and suggestions. maintenance. An architectural HP view, which contains ac- This work is funded and supported by the National Science tors HPA, composers CPR, and connectors HPC , can be Foundation under Grant CNS-0834701, by the National Secu- transformed into a single HP via transformation functions rity Agency, and by the Department of Defense under Contract of CPR and HPC . Given a view, it is possible to reuse No. FA8721-05-C-0003 with Carnegie Mellon University for its parts and express its properties in dL, thus the level the operation of the Software Engineering Institute, a federally of abstraction is elevated to components and systems from funded research and development center. individual statements. I have also defined an analysis to check whether a view has a proper compositional structure, e.g., 3 Available at github.com/bisc/active whether an actor violates the laws of causality by manipulating 4 nasa.gov/europa variables of another actor outside existing connectors. 5 lunar.cs.cmu.edu R EFERENCES [19] J. Sztipanovits, T. Bapty, S. Neema, L. Howard, and E. Jackson, “OpenMETA: A Model and Component-Based Design Tool Chain for [1] R. Rajkumar, I. Lee, L. Sha, and J. Stankovic, “Cyber-physical systems: Cyber-Physical Systems,” in From Programs to Systems The Systems The next computing revolution,” in 2010 47th ACM/IEEE Design Perspective in Computing (FPS 2014). Grenoble, France: Springer, Automation Conference (DAC), 2010, pp. 731–736. Apr. 2014. [2] Paul Gao, Russel Hensley, and Andreas Zielke, “A road map to the [20] A. Bhave, B. Krogh, D. Garlan, and B. Schmerl, “View Consistency in future for the auto industry,” McKinsey Quarterly, Oct. 2014. Architectures for Cyber-Physical Systems,” in 2011 IEEE/ACM Interna- [3] P. Derler, E. A. Lee, and A. L. Sangiovanni-Vincentelli, “Addressing tional Conference on Cyber-Physical Systems (ICCPS), Apr. 2011, pp. Modeling Challenges in Cyber-Physical Systems,” EECS Department, 151 –160. University of California, Berkeley, Tech. Rep. UCB/EECS-2011-17, [21] M.-Y. Nam, D. de Niz, L. Wrage, and L. Sha, “Resource allocation Mar. 2011. contracts for open analytic runtime models,” in Proc. of the 9th Inter- [4] J. Sztipanovits, X. Koutsoukos, G. Karsai, N. Kottenstette, P. Antsaklis, national Conference on Embedded Software, ser. EMSOFT ’11. New V. Gupta, B. Goodwine, J. Baras, and S. Wang, “Toward a Science of York, NY, USA: ACM, 2011, pp. 13–22. Cyber-Physical System Integration,” Proceedings of the IEEE, vol. 100, [22] D. Millward, “Smart traffic lights to stop speeders,” The Telegraph, no. 1, pp. 29–44, Jan. 2012. May 2011. [Online]. Available: http://www.telegraph.co.uk/motoring/ [5] M. Wolf and E. Feron, “What Don’T We Know About CPS Ar- news/8521769/Smart-traffic-lights-to-stop-speeders.html chitectures?” in Proceedings of the 52Nd Annual Design Automation [23] A. Rajhans, A. Bhave, I. Ruchkin, B. Krogh, D. Garlan, A. Platzer, Conference, ser. DAC ’15. New York, NY, USA: ACM, 2015, pp. and B. Schmerl, “Supporting Heterogeneity in Cyber-Physical Systems 80:1–80:4. Architectures,” IEEE Transactions on Automatic Control, vol. 59, no. 12, [6] A. Valukas, “Report to Board of Directors of General Motors Company pp. 3178–3193, Dec. 2014. Regarding Ignition Switch Recalls,” Jenner & Block, Tech. Rep., May [24] A. Rajhans, A. Bhave, S. Loos, B. Krogh, A. Platzer, and D. Garlan, 2014. Using Parameters in Architectural Views to Support Heterogeneous [7] P. Fradet, D. Metayer, and M. Perin, “Consistency Checking for Multiple Design and Verification, 2011, submitted for publication. View Software Architectures,” Software Engineering ESEC/FSE 99, vol. [25] I. Ruchkin, D. De Niz, S. Chaki, and D. Garlan, “Contract-based 1687, pp. 410–428, 1999. Integration of Cyber-physical Analyses,” in Proceedings of the 14th [8] A. Platzer, “Differential Dynamic Logic for Hybrid Systems,” Journal International Conference on Embedded Software, ser. EMSOFT ’14. of Automated Reasoning, vol. 41, no. 2, pp. 143–189, Aug. 2008. New York, NY, USA: ACM, 2014, pp. 23:1–23:10. [9] J. Magee and J. Kramer, Concurrency: State Models & Java Programs. [26] A. Pnueli, “The temporal logic of programs,” in 18th Annual Symposium Wiley, Apr. 1999. on Foundations of Computer Science, 1977, Oct. 1977, pp. 46–57. [10] E. A. Lee, “CPS Foundations,” in Proceedings of the 47th Design [27] D. D. Ruscio, I. Malavolta, H. Muccini, P. Pelliccione, and A. Pieran- Automation Conference, ser. DAC ’10. New York, NY, USA: ACM, tonio, “Model-Driven Techniques to Enhance Architectural Languages 2010, pp. 737–742. Interoperability,” in Fundamental Approaches to Software Engineering. [11] P. H. Feiler and D. P. Gluch, Model-Based Engineering with AADL: Springer Berlin Heidelberg, 2012, no. 7212, pp. 26–42. An Introduction to the SAE Architecture Analysis & Design Language, [28] M. Kessentini, H. Sahraoui, and M. Boukadoum, “Model Transformation 1st ed. Upper Saddle River, NJ: Addison-Wesley Professional, Oct. as an Optimization Problem,” in Model Driven Engineering Languages 2012. and Systems. Springer Berlin Heidelberg, 2008, no. 5301, pp. 159–173. [12] J. Dabney and T. L. Harman, Mastering SIMULINK 2. Upper Saddle [29] Z. Diskin, “Algebraic Models for Bidirectional Model Synchronization,” River, N.J.: Prentice Hall, 1998. in Model Driven Engineering Languages and Systems, ser. Lecture Notes [13] R. Alur, T. A. Henzinger, and H. Wong-toi, “Symbolic Analysis of in Computer Science. Springer Berlin Heidelberg, 2008, no. 5301, pp. Hybrid Systems,” 1997. 21–36. [14] I. Ruchkin, B. Schmerl, and D. Garlan, “Architectural Abstractions [30] P. Kaufmann, M. Kronegger, A. Pfandler, M. Seidl, and M. Widl, for Hybrid Programs,” in Proceedings of the 18th International ACM “A SAT-Based Debugging Tool for State Machines and Sequence SIGSOFT Symposium on Component-Based Software Engineering, ser. Diagrams,” in Software Language Engineering. Springer International CBSE ’15. New York, NY, USA: ACM, 2015, pp. 65–74. Publishing, Sep. 2014, no. 8706, pp. 21–40. [15] R. Mateescu, “Model Checking for Software Architectures,” in Software [31] B. Schmerl and D. Garlan, “AcmeStudio: Supporting Style-Centered Architecture. Springer Berlin Heidelberg, Jan. 2004, no. 3047, pp. 219– Architecture Development,” in Proceedings of the 26th International 224. Conference on Software Engineering, ser. ICSE ’04. Washington, DC, [16] A. Sangiovanni-Vincentelli, W. Damm, and R. Passerone, “Taming Dr. USA: IEEE Computer Society, 2004, pp. 704–705. Frankenstein: Contract-Based Design for Cyber-Physical Systems*,” [32] I. Ruchkin, D. De Niz, S. Chaki, and D. Garlan, “ACTIVE: A Tool for European Journal of Control, vol. 18, no. 3, pp. 217–238, 2012. Integrating Analysis Contracts,” in 5th Analytic Virtual Integration of [17] A. Rajhans and B. H. Krogh, “Compositional Heterogeneous Abstrac- Cyber-Physical Systems Workshop, Rome, Italy, Dec. 2014. tion,” in Proceedings of the 16th International Conference on Hybrid [33] P. Feiler, L. Wrage, J. Delange, and J. Siebel, “OSATE [Github],” Systems: Computation and Control, ser. HSCC ’13. New York, NY, 2015. [Online]. Available: https://github.com/osate USA: ACM, 2013, pp. 253–262. [34] I. Ruchkin, A. Rao, D. De Niz, S. Chaki, and D. Garlan, “Eliminating [18] C. Ptolemaeus, System Design, Modeling, and Simulation using Ptolemy Inter-Domain Vulnerabilities in Cyber-Physical Systems: An Analysis Ii. Ptolemy.org, Sep. 2013. Contracts Approach,” in Proc. of the First ACM Workshop on Cyber- Physical Systems Security & Privacy (CPS-SPC), Denver, Colorado, 2015.