%
% GENERATED FROM http://acme.able.cs.cmu.edu
% by : anonymous
% IP : ec2-18-222-23-166.us-east-2.compute.amazonaws.com
% at : Wed, 02 Apr 2025 22:59:19 -0400 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}
}