 |
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), the Defense Advanced Research Projects Agency (DARPA), 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.
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.
Relevant Papers:
- P. 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.
- C. 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.
- P. 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.
- P. 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.
Contract-Based Requirement Engineering for System Design
Safety-critical and time-critical systems pose several design and verification challenges. The design space is often too large and heterogeneous to be efficiently explored with strong guarantees of correctness, dependability, and compliance with regulations. Different stages of the design process tend to rely on domain-specific languages and tools that are poorly inter-operable, making it hard to combine different analysis methods and design artifacts. Modern requirement-management tools are still predominantly centered on text-based languages, which creates opportunities for ambiguities, redundancies, and potential conflicts. While virtual prototyping and model-based engineering tools are the de facto standard for system development, the concept design phase largely remains a manual process.
An approach based on contracts, mathematical models of the interfaces between the components of a design and their environments, can offer effective 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. The CHASE (Contract-based Heterogeneous Analysis and System Exploration) project investigates a contract-based framework for requirement capture, formalization, and validation for system design. CHASE aims to provide a laboratory for research and experimentation with assume-guarantee reasoning, contract-based design, and requirement engineering, bridging the gap between the theory of contracts and the development of methods that support them and enable their adoption in system design.
Relevant Papers:
- P. Nuzzo, M. Lora, Y. Feldman, A. L. Sangiovanni-Vincentelli, “CHASE: Contract-Based Requirement Engineering for Cyber-Physical System Design,” Proc. Design Automation and Testing in Europe Conference (DATE), pp. 839-844, Mar. 2018.
Further References on Contract-Based Design
- A Platform-Based Design Methodology with Contracts and Related Tools for the Design of Cyber-Physical Systems (Proc. IEEE 2015)
- Compositional Design of Cyber-Physical Systems Using Contracts (Ph.D. Dissertation, Aug. 2015)
- Smart Buildings in the Smart Grid: Contract-Based Design of an Integrated Energy Management System (in “Cyber Physical Systems Approach to Smart Electric Power Grid”, Power Systems, Springer 2015)
- A Contract-Based Framework for Integrated Demand-Response Management in Smart Grids (BuildSys 2015)
- Methodology and Tools for Next Generation Cyber-Physical Systems: The iCyPhy Approach (INCOSE 2015)
- Contract-Based Methodology for Aircraft Electric Power System Design (IEEE Access, 2014)
- Are Interface Theories Equivalent to Contract Theories? (MEMOCODE 2014)
- Metronomy: A Function-Architecture Co-simulation Framework for Timing Verification of Cyber-Physical Systems (CODES+ISSS 2014)
- Contract-Based Design of Control Protocols for Safety-Critical Cyber-Physical Systems (DATE 2014)
- Library-Based Scalable Refinement Checking for Contract-Based Design (DATE 2014)
- Methodology for the Design of Analog Integrated Interfaces Using Contracts (IEEE Sensors Journal, 2012)