The design of complex cyber-physical system architectures is often hierarchical. System specifications are mapped to an implementation layer via a stepwise refinement process involving multiple intermediate layers. These layers may capture different functionalities, and the orchestration of a variety of heterogeneous techniques suited to each layer may be required to achieve the overall design objectives. Due to their heterogeneity, ensuring traceability and verifiability of such architectures is a challenging problem. In this article, we present a correct-by-construction methodology for designing heterogeneous layered architectures. We capture the specifications at each layer with assume-guarantee contracts , a specification paradigm which can encompass a variety of modeling formalisms. We then use the notion of contract embeddings to define specification refinement , rigorously and traceably mapping specifications across layers modeled with heterogeneous formalisms. We instantiate our methodology on the design of layered control architectures (LCAs), resulting in a novel approach that can verifiably orchestrate domain-specific techniques to satisfy both global planning and local safety requirements. In the context of LCAs, we derive necessary conditions for correct specification refinement and results for compositional realization of control safety specifications. We illustrate our design methodology on a motivating example and a case study derived from robotic mission planning and control.

The design of complex mission-critical systems often follows a layered approach, which may lead to complicated, multilevel, multiviewpoint requirement hierarchies. This heterogeneity makes it challenging to guarantee the traceability of the requirements across levels of abstraction and, consequently, the satisfaction of the requirements by a system implementation, especially when requirements at different abstraction levels are expressed using different mathematical formalisms and modeling languages. In this article, we address this challenge by introducing heterogeneous hierarchical contract networks (HHCNs), a formal model based on a graph of assume-guarantee contracts, for capturing and analyzing heterogeneous requirement hierarchies. We formulate the requirement traceability validation problem in terms of contract refinement relations between nodes in an HHCN. We then define contract embeddings to enable reasoning about refinements across levels of abstraction in the HHCN that are expressed using heterogeneous formalisms. Contract embeddings leverage the notion of conservative approximation to rigorously map contracts across levels of abstraction while ensuring that refinement is preserved independently of the formalism to which the contracts are mapped. We illustrate their effectiveness on a case study motivated by a multiagent autonomous lunar rover mission.

The proliferation of artificial intelligence based systems in all walks of life raises concerns about their safety and robustness, especially for cyber-physical systems including multiple machine learning components. In this paper, we introduce robustness contracts as a framework for compositional specification and reasoning about the robustness of cyber-physical systems based on neural network (NN) components. Robustness contracts can encompass and generalize a variety of notions of robustness which were previously proposed in the literature. They can seamlessly apply to NN-based perception as well as deep reinforcement learning (RL)-enabled control applications. We present a sound and complete algorithm that can efficiently verify the satisfaction of a class of robustness contracts on NNs by leveraging notions from Lagrangian duality to identify system configurations that violate the contracts. We illustrate the effectiveness of our approach on the verification of NN-based perception systems and deep RL-based control systems.