Papers

file

Visible to the public Contract-Based Integration of Cyber-Physical Analyses

Abstract: Developing cyber-physical systems involves multiple engineering domains, e.g., timing, logical correctness, thermal resilience, and mechanical stress. In today's industrial practice, these domains rely on multiple analyses to obtain and verify critical system properties. Domain differences make the analyses abstract away interactions among themselves, potentially invalidating the results. Specifically, one challenge is to ensure that an analysis is never applied to a model that violates the assumptions of the analysis.

file

Visible to the public ACTIVE: A Tool for Integrating Analysis Contracts

Abstract: Development of modern Cyber-Physical Systems (CPS) relies 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.

file

Visible to the public Architectural Abstractions for Hybrid Programs

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.

file

Visible to the public Supporting Heterogeneity in Cyber-Physical Systems Architectures

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.

file

Visible to the public Stochastic differential dynamic logic for stochastic hybrid programs

file

Visible to the public Logics of dynamical systems

file

Visible to the public Formal verification of distributed aircraft controllers

file

Visible to the public Adaptive Cruise Control-Hybrid Distributed and Now Formally Verified

Title
Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified

file

Visible to the public Safe Intersections At the Crossing of Hybrid Systems and Verification

Title
Safe Intersections: At the Crossing of Hybrid Systems and Verification