Skip to content

Formalisms for Cyber-Physical System Specification, Analysis, and Design

System design cannot rely on ad hoc tweaking techniques. A rigorous design discipline is crucial to boost productivity and enforce design correctness.

We are investigating modeling paradigms, algorithms, design methodologies, design flows, and supporting tools to enable compositional and hierarchical design of complex cyber-physical systems, with emphasis on systems enabled by artificial intelligence. We show that a contract-based approach can provide a formal foundation for system design methodologies encompassing both horizontal and vertical integration steps.

Our research in this area is supported by the National Science Foundation (NSF) and the Office of Naval Research (ONR).

High-Assurance Design of Learning-Enabled Cyber-Physical Systems with Deep Contracts (NSF CAREER Award)

Next-generation cyber-physical systems (CPSs) will increasingly rely on machine learning algorithms with the promise of enhancing human capabilities in a variety of applications, from autonomous driving to robotics and industrial automation. However, the undesired outcomes of recent deployments, such as the accidents involving semi-autonomous vehicles, raise questions about the design principles needed to build learning-enabled systems that are safe. This project investigates novel mathematical methods for the design of “intelligent,” autonomous, cyber-physical systems that are enabled by machine learning components. We explore techniques to rigorously model and analyze the sources of uncertainty and approximation introduced by learning components and enable the construction of systems with high guarantees of correctness in a scalable and modular way. We aim to provide a unifying framework for understanding a number of robust and fault-tolerant design approaches that are currently based mostly on ad hoc solutions.

We are developing a compositional framework for reasoning about the probabilistic behaviors of learning-enabled CPSs by relying on stochastic models of the interfaces between the components and their environments, termed deep contracts, together with rigorous rules for composing and refining them. Deep contracts will leverage rich, logic-based stochastic specification formalisms to express and propagate computationally tractable representations of uncertainty at different abstraction levels, and novel computational tools to efficiently solve contract-based verification and synthesis problems. Theory, algorithms, and tools will be developed and evaluated in the context of autonomous driving and other autonomous CPS applications.

Relevant Papers:

  • Nuzzo, N. Bajaj, M. Masin, D. Kirov, R. Passerone, A. Sangiovanni-Vincentelli, “Optimized Selection of Reliable and Cost-Effective Safety-Critical System Architectures,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, to appear, 2020.
  • Oh, E. Kang, S. Shiraishi, P. Nuzzo, “Optimizing Assume-Guarantee Contracts for Cyber-Physical System Design,” Proc. Design Automation and Testing in Europe Conference (DATE), pp. 246-251, Mar. 2019.
  • Nuzzo, J. Li, A. L. Sangiovanni-Vincentelli, Y. Xi, D. Li, “Stochastic Assume-Guarantee Contracts for Cyber-Physical System Design,” ACM Trans. Embedded Computing Syst., vol. 18, no. 1, article 2, 26 pages, Jan. 2019.
  • Nuzzo, A. L. Sangiovanni-Vincentelli, “Hierarchical System Design with Vertical Contracts,” in Principles of Modeling, Lecture Notes in Computer Science, vol. 10760, Springer, pp. 360-382, Jul. 2018.

CHASE.AI: Compositional and Hierarchical verificAtion and Synthesis of systems Enabled by Artificial Intelligence

Cyber-physical systems are increasingly reliant on artificial intelligence (AI)-enabled components for enhanced perception, situational awareness, and adaptation to unstructured and uncertain environments. This trend has substantially increased system complexity, and traditional methods for system verification and validation, aiming to provide strong guarantees of correctness and dependability, have become inadequate. This project aims to develop CHASE.AI, a methodology, supported by tools, for scalable verification and validation of AI-enabled systems by leveraging: compact abstractions of different AI components to efficiently reason about multiple design objectives in complex closed-loop systems; scalable algorithmic techniques to generate correct implementations of AI-enabled components from high-level specifications; hierarchical and incremental system verification methods; and modular monitoring algorithms for runtime design assurance. CHASE.AI adopts a modeling approach based on contracts, offering mechanisms for rigorous abstraction, composition, and reuse, which are key to enable scalable verification of complex systems and determine the correctness of designs made of independently developed sub-systems.

Further References on Contract-Based Design