% % GENERATED FROM http://acme.able.cs.cmu.edu % by : anonymous % IP : ec2-18-117-156-170.us-east-2.compute.amazonaws.com % at : Thu, 21 Nov 2024 16:31:26 -0500 GMT % % Selection : Author: Ivan_Ruchkin % @InProceedings{Garlan/EUA/2012, AUTHOR = {Garlan, David and Dwivedi, Vishal and Ruchkin, Ivan and Schmerl, Bradley}, TITLE = {Foundations and Tools for End-User Architecting}, YEAR = {2012}, BOOKTITLE = {Large-Scale Complex IT Systems. Development, Operation and Management, 17th Monterey Workshop 2012, Oxford, UK, March 19-21, 2012}, VOLUME = {7539}, PAGES = {157-182}, EDITOR = {Garlan, David and Calinescu, Radu}, SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {Springer}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/EUA-LNCS.pdf}, ABSTRACT = {Within an increasing number of domains an important emerging need is the ability for technically naive users to compose computational elements into novel configurations. Examples include astronomers who create new analysis pipelines to process telescopic data, intelligence analysts who must process diverse sources of unstructured text to discover socio-technical trends, and medical researchers who have to process brain image data in new ways to understand disease pathways. Creating such compositions today typically requires low-level technical expertise, limiting the use of computational methods and increasing the cost of using them. In this paper we describe an approach -- which we term end-user architecting -- that exploits the similarity between such compositional activities and those of software architects. Drawing on the rich heritage of software architecture languages, methods, and tools, we show how those techniques can be adapted to support end users in composing rich computational systems through domain-specific compositional paradigms and component repositories, without requiring that they have knowledge of the low-level implementation details of the components or the compositional infrastructure. Further, we outline a set of open research challenges that the area of end-user architecting raises.}, NOTE = {Book Reference: http://www.springer.com/computer/swe/book/978-3-64234058-1}, KEYWORDS = {End-user Architecture, Landmark, Service Composition, SORASCS} } @Article{Rajhans/TAC/2013, AUTHOR = {Rajhans, Akshay and Bhave, Ajinkya Y. and Ruchkin, Ivan and Krogh, Bruce and Garlan, David and Platzer, Andre and Schmerl, Bradley}, TITLE = {Supporting Heterogeneity in Cyber-Physical Systems Architectures}, YEAR = {2014}, MONTH = {December}, JOURNAL = {IEEE Transactions on Automatic Control}, VOLUME = {59}, NUMBER = {12}, PAGES = {3178--3193}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/TAS-Dec-2014.pdf}, ABSTRACT = {Cyber-physical systems (CPS) are heterogeneous, because they tightly couple computation, communication and control along with physical dynamics, which are traditionally considered separately. Without a comprehensive modeling formalism, model-based development of CPS involves using a multitude of models in a variety of formalisms that capture various aspects of the system design, such as software design, networking design, physical models, and protocol design. Without a rigorous unifying framework, system integration and integration of the analysis results for various models remains ad hoc. In this paper, we propose a multi-view architecture framework that treats models as views of the underlying system structure and uses structural and semantic mappings to ensure consistency and enable system-level veri?cation from that of the models in a hierarchical and compositional manner. Throughout the paper, the theoretical concepts are illustrated using two examples, an automotive intersection collision avoidance system and a quadrotor.}, NOTE = {Also available at http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6882828}, KEYWORDS = {Cyberphysical Systems, Landmark} } @TechReport{ruchkin_architectural_2014, AUTHOR = {Ruchkin, Ivan and Dwivedi, Vishal and Garlan, David and Schmerl, Bradley}, TITLE = {Architectural Modeling of Ozone Widget Framework End-User Compositions}, YEAR = {2014}, MONTH = {June}, NUMBER = {CMU-ISR-14-108}, ADDRESS = {Pittsburgh, PA}, TYPE = {Technical Report}, INSTITUTION = {Institute for Software Research, Carnegie Mellon University}, URL = {http://reports-archive.adm.cs.cmu.edu/anon/isr2014/abstracts/14-108.html}, ABSTRACT = {Ozone Widget Framework (OWF) is an event-based web platform for lightweight integration of widget applications. This technical report presents a formal model of OWF’s widget composition mechanism. First, we present a detailed description of Ozone’s end user composition mechanism. Then, we describe our architectural modeling approach and its value for analysis of OWF widget compositions. We go through the process of creating an architectural style to represent assemblies of Ozone widgets, reviewing modeling decision points and style alternatives.} } @InProceedings{2014/Ruchkin/CBI, AUTHOR = {Ruchkin, Ivan and De Niz, Dio and Chaki, Sagar and Garlan, David}, TITLE = {Contract-Based Integration of Cyber-Physical Analyses}, YEAR = {2014}, MONTH = {12-17 October}, BOOKTITLE = {Embedded Systems Week}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/paper-camera-ready-ieee-verified-178-EM82.pdf}, ABSTRACT = {Developing cyber-physical systems involves creating systems with properties from multiple domains, e.g., timing, logical correctness, thermal resilience, aerodynamics, and mechanical stress. In todayďż˝s industrial practice, multiple analyses are used to obtain and verify such properties. Unfortunately, given that these analyses originate from different scientific domains, they abstract away interactions among themselves, risking the invalidation of their results. Specifically, one challenge is to ensure that an analysis is never applied to a model that violates its assumptions. Since such violation can originate from the updating of the model by another analysis, analyses must be executed in the correct order. Another challenge is to do this soundly and scalably over models of realistic complexity and diverse set of analyses. To address these challenges, we develop an analysis integration approach that uses contracts to specify dependencies between analyses, determine their correct orders of application, and specify and verify applicability conditions across multiple domains. We present an implementation of our approach, and demonstrate its effectiveness, extensibility, and scalability.}, KEYWORDS = {Cyberphysical Systems, Landmark} } @InProceedings{ruchkin/active/2014, AUTHOR = {Ruchkin, Ivan and De Niz, Dio and Chaki, Sagar and Garlan, David}, TITLE = {ACTIVE: A Tool for Integrating Analysis Contracts}, YEAR = {2014}, MONTH = {2 December}, BOOKTITLE = {The 5th Analytic Virtual Integration of Cyber-Physical Systems Workshop}, ADDRESS = {Rome, Italy}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/avicps14-camera-ready.pdf}, ABSTRACT = {Development of modern Cyber-Physical Systems (CPS) re- lies on a number of analysis tools to verify critical properties. The Architecture Analysis and Design Language (AADL) standard provides a common architectural model to which multiple CPS analyses can be applied. Unfortunately, interaction between these analyses can invalidate their results. In this paper we present ACTIVE, a tool developed within the OSATE/AADL infrastructure to solve this problem. We analyze the problems that occur when multiple analyses are applied to an AADL model and how these problems invalidate analysis results. Interactions between analyses, implemented as OSATE plugins, are formally described in ACTIVE in order to enable automatic verification. In particular, these interactions are captured in an analysis contract consisting of inputs, outputs, assumptions, and guarantees. The inputs and outputs help determine the correct order of execution of the plugins. Assumptions capture the conditions that must be valid in order to execute an analysis plugin, while guarantees are conditions that are expected to be valid afterwards. ACTIVE allows the use of any generic verification tool (e.g., a model checker) to validate these conditions. To coordinate these activities our tool uses two components: ACTIVE EXECUTER and ACTIVE VERIFIER. ACTIVE EXECUTER invokes the analysis plugins in the required order and uses ACTIVE VERIFIER to check assumptions and guarantees. ACTIVE VERIFIER identifies and executes the verification tool that needs to be invoked based on the target formula. Together, they ensure that plugins are always executed in the correct order and under the correct conditions, guaranteeing correct results. To the best of our knowledge, ACTIVE is the first extensible framework that integrates independently-developed analysis plugins ensuring provably-correct interactions.}, KEYWORDS = {Cyberphysical Systems, Formal Methods} } @InProceedings{Ruchkin:2015:AAHP, AUTHOR = {Ruchkin, Ivan and Schmerl, Bradley and Garlan, David}, TITLE = {Architectural Abstractions for Hybrid Programs}, YEAR = {2015}, MONTH = {4-8 May}, BOOKTITLE = {Proceedings of the 18th International ACM Sigsoft Symposium on Component-Based Software Engineering (CBSE 2015)}, ADDRESS = {Montreal, QC, Canada}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/AAHP.pdf}, ABSTRACT = {Modern cyber-physical systems interact closely with continuous physical processes like kinematic movement. Software component frameworks do not provide an explicit way to represent or reason about these processes. Meanwhile, hybrid program models have been successful in proving critical properties of discrete-continuous systems. These programs deal with diverse aspects of a cyber-physical system such as controller decisions, component communication protocols, and mechanical dynamics, requiring several programs to address the variation. However, currently these aspects are often intertwined in mostly monolithic hybrid programs, which are difficult to understand, change, and organize. These issues can be addressed by component-based engineering, making hybrid modeling more practical. This paper lays the foundation for using architectural models to provide component-based benefits to developing hybrid programs. We build formal architectural abstractions of hybrid programs and formulas, enabling analysis of hybrid programs at the component level, reusing parts of hybrid programs, and automatic transformation from views into hybrid programs and formulas. Our approach is evaluated in the context of a robotic collision avoidance case study. }, NOTE = {CBSE Best Paper Award}, KEYWORDS = {Architecture View Consistency, Cyberphysical Systems, Landmark, Software Architecture} } @InProceedings{Ruchkin/2015/AC-SPC, AUTHOR = {Ruchkin, Ivan and Rao, Ashwini and De Niz, Dio and Chaki, Sagar and Garlan, David}, TITLE = {Eliminating Inter-Domain Vulnerabilities in Cyber-Physical Systems: An Analysis Contracts Approach}, YEAR = {2015}, MONTH = {16 October}, BOOKTITLE = {Proceedings of the First ACM Workshop on Cyber-Physical Systems Security and Privacy}, ADDRESS = {Denver, Colorado}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/AC for SPC-camera-ready-preprint-v2.pdf}, ABSTRACT = {Designing secure cyber-physical systems (CPS) is a particularly difficult task since security vulnerabilities stem not only from traditional cybersecurity concerns, but also physical ones as well. Many of the standard methods for CPS design make strong and unverified assumptions about the trustworthiness of physical devices, such as sensors. When these assumptions are violated, subtle inter-domain vulnerabilities are introduced into the system model. In this paper we propose to use formal specification of analysis contracts to expose security assumptions and guarantees of analyses from reliability, control, and sensor security domains. We show that this specification allows us to determine where these assumptions are violated or ignore important failure modes that open the door to malicious attacks. We demonstrate how this approach can help discover and prevent vulnerabilities in a self-driving car example.}, KEYWORDS = {Cyberphysical Systems, Science of Security} } @InProceedings{Ruchkin/2015/loops, AUTHOR = {Ruchkin, Ivan and Schmerl, Bradley and Garlan, David}, TITLE = {Analytic Dependency Loops in Architectural Models of Cyber-Physical Systems}, YEAR = {2015}, MONTH = {28 September}, BOOKTITLE = {Proceedings of the 8th International Workshop on Model-based Architecting of Cyber-Physical and Embedded Systems}, ADDRESS = {Ottawa, Canada}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/MBA-CPS.pdf}, ABSTRACT = {Rigorous engineering of safety-critical Cyber- Physical Systems (CPS) requires integration of heterogeneous modeling methods from different disciplines. It is often necessary to view this integration from the perspective of analyses – algorithms that read and change models. Although analytic integration supports formal contract-based verification of model evolution, it suffers from the limitation of analytic dependency loops. Dependency loops between analyses cannot be resolved based on the existing contract-based verification. This paper makes a step towards using rich architectural description to resolve circular analytic dependencies. We characterize the dependency loop problem and discuss three algorithmic approaches to resolving such loops: analysis iteration, constraint solving, and genetic search. These approaches take advantage of information in multi-view architectures to resolve analytic dependency loops.}, KEYWORDS = {Architecture View Consistency, Cyberphysical Systems} } @InProceedings{2015/Ruchkin/MODELS, AUTHOR = {Ruchkin, Ivan}, TITLE = {Architectural and Analytic Integration of Cyber-Physical System Models}, YEAR = {2015}, MONTH = {30 September - 2 October}, BOOKTITLE = {ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems, ACM Student Research Award Competition}, ADDRESS = {Ottawa, Canada}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/SRC-131.pdf}, ABSTRACT = {Modeling methods for Cyber-Physical Systems (CPS) originate in various engineering fields, and are difficult to use together due to their heterogeneity. Inconsistencies between mutually oblivious models and analyses often lead to implicit design errors, which may cause catastrophic failures of critical CPS. Such consistency issues are not fully solved by the state-of-the-art integration methods, which lack generality, formal guarantees, and effectiveness. To overcome these limitations and achieve better integration, this paper outlines a two-level integration approach based on architectural views and analysis contracts. In particular, this paper proposes languages and algorithms to specify and verify important integration properties, such as correct analysis execution and rich consistency of architectural views. According to the results to date, this approach shows promise in detection and prevention of implicit errors, which would be difficult to fix otherwise. }, NOTE = {Gold Medal Winner}, KEYWORDS = {Cyberphysical Systems} } @InProceedings{2016/Ruchkin/integration, AUTHOR = {Ruchkin, Ivan}, TITLE = {Integration Beyond Components and Models: Research Challenges and Directions}, YEAR = {2016}, MONTH = {April}, BOOKTITLE = {Proceedings of the 3rd Architecture Centric Virtual Integration Workshop}, ADDRESS = {Venice, Italy}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/acvi-2016.pdf}, ABSTRACT = {Recent research in embedded and cyber-physical systems has developed theories and tools for integration of heterogeneous components and models. These efforts, although important, are insufficient for high-quality and error-free systems integration since inconsistencies between system elements may stem from factors not directly represented in models (e.g., analysis tools and expert disagreements). Therefore, we need to broaden our perspective on integration, and devise approaches in three novel directions of integration: modeling methods, data sets, and humans. This paper summarizes the latest advances, and discusses those directions and associated challenges in integration for cyber-physical systems.}, KEYWORDS = {Cyberphysical Systems, Software Architecture} } @InProceedings{MARTCPS16, AUTHOR = {Ruchkin, Ivan and Samuel, Selva and Schmerl, Bradley and Rico, Amanda and Garlan, David}, TITLE = {Challenges in Physical Modeling for Adaptation of Cyber-Physical Systems}, YEAR = {2016}, MONTH = {12-14 December}, BOOKTITLE = {Workshop on MARTCPS Models at Runtime and Networked Control for Cyber Physical Systems at IEEE World Forum on the Internet of Things}, ADDRESS = {Reston, Virginia}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/MARTCPS2016.pdf}, ABSTRACT = {Cyber-physical systems (CPSs) mix software, hardware, and physical aspects with equal importance. Typically, the use of models of such systems during run time has concentrated only on managing and controlling the cyber (software) aspects. However, to fully realize the goals of a CPS, physical models too have to be treated as first-class models. This approach gives rise to three main challenges: (a) identifying and integrating physical and software models with different characteristics and semantics; (b) obtaining instances of physical models at a suitable level of abstraction for adaptation; and (c) using and adapting physical models to control CPSs. In this position paper, we elaborate on these three challenges and describe our vision of making physical models first-class entities in adaptation. We illustrate this vision in the context of power adaptation for a service robotic system.}, NOTE = {Winner of the IEEE World Forum on the Internet of Things Best Paper Award}, KEYWORDS = {Cyberphysical Systems} } @InProceedings{2017:Pandey:HybridPlanningFormalization, AUTHOR = {Pandey, Ashutosh and Ruchkin, Ivan and Schmerl, Bradley and C\'{a}mara, Javier}, TITLE = {Towards a Formal Framework for Hybrid Planning in Self-Adaptation}, YEAR = {2017}, MONTH = {22-23 May}, BOOKTITLE = {Proceedings of the 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2017)}, ADDRESS = {Buenos Aires, Argentina}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/hybrid-planning-seams2017.pdf}, ABSTRACT = {Approaches to self-adaptation face a fundamental trade-off between quality and timeliness in decision-making. Due to this trade-off, designers of self-adaptive systems often have to find a fixed and suboptimal compromise between these two requirements. Recent work has proposed the hybrid planning approach that can resolve this trade-off dynamically and potentially in an optimal way. The promise of hybrid planning is to combine multiple planners at run time to produce adaptation plans of the highest quality within given time constraints. However, since decision-making approaches are complex and diverse, the problem of combining them is even more difficult, and no frameworks for hybrid planning. This paper makes an important step in simplifying the problem of hybrid planning by formalizing it and decomposing it into four simpler subproblems. These formalizations will serve as a foundation for creating and evaluating engineering solutions to the hybrid planning problem.}, KEYWORDS = {Planning, Self-adaptation} } @InProceedings{Ruchkin/2018/IPL, AUTHOR = {Ruchkin, Ivan and Sunshine, Joshua and Iraci, Grant and Schmerl, Bradley and Garlan, David}, TITLE = {IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems}, YEAR = {2018}, MONTH = {15-17 July}, BOOKTITLE = {22nd International Symposium on Formal Methods (FM2018)}, ADDRESS = {Oxford, UK}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/fm2018-paper-camera-ready-1.pdf}, ABSTRACT = {Design and verification of modern systems requires diverse models, which often come from a variety of disciplines, and it is challenging to manage their heterogeneity – especially in the case of cyber-physical systems. To check consistency between models, recent approaches map these models to flexible static abstractions, such as architectural views. This model integration approach, however, comes at a cost of reduced expressiveness because complex behaviors of the models are abstracted away. As a result, it may be impossible to automatically verify important behavioral properties across multiple models, leaving systems vulnerable to subtle bugs. This paper introduces the Integration Property Language (IPL) that improves integration expressiveness using modular verification of properties that depend on detailed behavioral semantics while retaining the ability for static system-wide reasoning. We prove that the verification algorithm is sound and analyze its termination conditions. Furthermore, we perform a case study on a mobile robot to demonstrate IPL is practically useful and evaluate its performance.}, NOTE = {Appendices}, KEYWORDS = {Cyberphysical Systems, Formal Methods, Model Checking} } @Unpublished{2018:Pandey:Hybrid, AUTHOR = {Pandey, Ashutosh and Ruchkin, Ivan and Schmerl, Bradley and C\'{a}mara, Javier and Garlan, David}, TITLE = {Formalizing the Hybrid Planning Problem for Self-Adaptation}, YEAR = {2019}, ABSTRACT = {Planning approaches in self-adaptation face the fundamental trade-off between quality and timeliness of adaptation plans. Due to this trade-off, today designers often have to compromise between a planning approach that is quick to find a plan and an approach that is slow but finds a quality plan. To deal with this trade-off, researchers have proposed a hybrid planning approach that combines more than one planning approaches to find a balance between quality and timeliness. However, the diversity of planning approaches makes the problem of hybrid planning complex and multi-faceted. This paper advances the theory of hybrid planning by formalizing the central concepts and four subproblems of hybrid planning. This formalization can serve as a foundation for not only understanding and comparing existing hybrid planners, but also for developing new hybrid planners in the future. Moreover, to illustrate practicality of the formal model, the paper uses it to analyze two hybrid planning instantiations that have shown to effective in their respective contexts. Furthermore, grounded on the formal model, the paper formalizes explicit/implicit assumptions about these instantiations that must hold for them to be sound.}, NOTE = {Submitted for publication}, KEYWORDS = {Formal Methods, Planning, Self-adaptation} } @Misc{2018:Ruchkin:IPL, AUTHOR = {Ruchkin, Ivan and Sunshine, Joshua and Iraci, Grant and Schmerl, Bradley and Garlan, David}, TITLE = {Appendix for IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems}, YEAR = {2018}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/fm2018-appendix.pdf}, NOTE = {Paper Reference} } @Article{2019:IEEESoftware:BRASS, AUTHOR = {Aldrich, Jonathan and Garlan, David and K\"astner, Christian and Le Goues, Claire and Mohseni-Kabir, Anahita and Ruchkin, Ivan and Samuel, Selva and Schmerl, Bradley and Timperley, Christopher Steven and Veloso, Manuela and Voysey, Ian and Biswas, Joydeep and Guha, Arjun and Holtz, Jarrett and C\'{a}mara, Javier and Jamshidi, Pooyan}, TITLE = {Model-Based Adaptation for Robotics Software}, YEAR = {2019}, MONTH = {March}, JOURNAL = {IEEE Software}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/brass-mars-ieee-software2019.pdf}, ABSTRACT = {We have developed model-based adaptation, an approach that leverages models of software and its environment to enable automated adaptation. The goal of our approach is to build long-lasting mobile software systems that can effectively adapt to changes in their environment.}, KEYWORDS = {Self-adaptation} } @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} } @InProceedings{2020:Pandey:Hybrid, AUTHOR = {Pandey, Ashutosh and Ruchkin, Ivan and Schmerl, Bradley and Garlan, David}, TITLE = {Hybrid Planning Using Learning and Model Checking for Autonomous Systems}, YEAR = {2020}, MONTH = {19-23 August}, BOOKTITLE = {Proceedings of the 2020 IEEE Conference on Autonomic Computing and Self-organizing Systems (ACSOS)}, ADDRESS = {Washington, D.C.}, ABSTRACT = {Self-adaptive software systems rely on planning to make adaptation decisions autonomously. Planning is required to produce high-quality adaptation plans in a timely manner; however, quality and timeliness of planning are conflicting in nature. This conflict can be reconciled with hybrid planning, which can combine reactive planning (to quickly provide an emergency response) with deliberative planning that take time but determine a higher-quality plan. While often effective, reactive planning sometimes risks making the situation worse. Hence, a challenge in hybrid planning is to decide whether to invoke reactive planning until the deliberative planning is ready with a high-quality plan. To make this decision, this paper proposes a novel learning-based approach. We demonstrate that this learning-based approach outperforms existing techniques that are based on specifying fixed conditions to invoke reactive planning in two domains: enterprise cloud systems and unmanned aerial vehicles.}, NOTE = {Supplemental Material | Presentation Video}, KEYWORDS = {Formal Methods, Machine Learning, Self-adaptation} } @InProceedings{2021:SISSY, AUTHOR = {Weyns, Danny and Bures, Tomas and Calinescu, Radu and Craggs, Barnaby and Fitzgerald, John and Garlan, David and Nuseibeh, Bashar and Pasquale, Liliana and Rashid, Awais and Ruchkin, Ivan and Schmerl, Bradley}, TITLE = {Six Software Engineering Principles for Smarter Cyber-Physical Systems}, YEAR = {2021}, MONTH = {27 September}, BOOKTITLE = {Proceedings of the Workshop on Self-Improving System Integration}, ABSTRACT = {Cyber-Physical Systems (CPS) integrate computational and physical components. With the digitisation of society and industry and the progressing integration of systems, CPS need to become “smarter” in the sense that they can adapt and learn to handle new and unexpected conditions, and improve over time. Smarter CPS present a combination of challenges that existing engineering methods have difficulties addressing: inter- twined digital, physical and social spaces, need for heterogeneous modelling formalisms, demand for context-tied cooperation to achieve system goals, widespread uncertainty and disruptions in changing contexts, inherent human constituents, and continuous encounter with new situations. While approaches have been put forward to deal with some of these challenges, a coherent perspective on engineering smarter CPS is lacking. In this paper, we present six engineering principles for addressing the challenges of smarter CPS. As smarter CPS are software-intensive systems, we approach them from a software engineering perspective with the angle of self-adaptation that offers an effective approach to deal with run-time change. The six principles create an integrated landscape for the engineering and operation of smarter CPS.}, KEYWORDS = {Cyberphysical Systems} }