Constrained Markov decision processes (CMDPs) models are increasingly important in many applications with multiple objectives. When the model is unknown and must be learned online, it is desirable to ensure that the constraint is met, or at least the violation is bounded with time. In recent literature, progress has been made on this very challenging problem but with either unsatisfactory assumptions such as the knowledge of a safe policy, or have high cumulative regret. We propose the Safe-PSRL (posterior sampling-based RL) algorithm that does not need such assumptions and yet performs very well, both in terms of theoretical regret bounds as well as empirically. The algorithm efficiently trades-off exploration and exploitation using posterior sampling-based exploration, and yet provably suffers only bounded constraint violation using carefully-crafted pessimism. We establish a sub-linear $\tilde{O}(H^{2.5}\sqrt{|S|^2|A|K})$ upper bound on the Bayesian objective regret along with a bounded, i.e., $\tilde{O}(1)$ constraint-violation regret over $K$ episodes for an $|S|$-state, $|A|$-action, and $H$ horizon CMDP which improves over state-of-the-art algorithms for the same setting.

Ensuring fairness is essential for ethical decision-making in various domains. Informally, a neural network is considered fair if and only if it treats similar individuals similarly in a given task. We introduce FaVeR (Fairness Verification and Repair), a framework for efficiently verifying and repairing pre-trained neural networks with respect to individual fairness properties. FaVeR ensures fairness via iterative search of high-sensitivity neurons and backward adjustment of their weights, guided by counterexamples generated from fairness verification using satisfiability modulo convex programming. By addressing fairness at the neuron level, FaVeR minimizes the impact of neural network repair on the overall performance. Experimental evaluations on common fairness datasets show that FaVeR achieves a 100% fairness repair rate across all models, with accuracy reduction of less than 2.27%. Moreover, its significantly lower average runtime makes it suitable for practical applications.

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 DeFacto project, supported by the European Commission via a Marie Skłodowska-Curie Global Individual Fellowship, tackles the complexity arising from the transformation of industrial manufacturing systems into intricate cyber-physical systems. This evolution offers unprecedented opportunities but also poses intellectual and engineering challenges. DeFacto aims to advance the design automation of cyber-physical production systems by developing innovative modeling paradigms, scalable algorithms, software architectures, and tools. In the DeFacto approach, production systems are managed through service-oriented manufacturing software architectures. System-level models capture the features and the requirements of production systems, representing both production and computational processes as services provided by the infrastructure. Methodologies for system analysis and optimization rely on compositional abstractions of system behaviors grounded in assume-guarantee contracts. This paper outlines key research endeavors, findings, and lessons learned from the DeFacto project.

We present ContrArc, a methodology for the exploration of cyber-physical system architectures aiming to minimize a cost function while adhering to a set of heterogeneous constraints. We assume a system topology, defined as a graph, where components (nodes) are selected from an implementation library, and connections between components (edges) are drawn from a finite set of possible connection choices. ContrArc uses assume-guarantee contracts to formalize different viewpoints in the system requirements, such as timing and power consumption, as well as the interface of different components, and translate the exploration problem into a mixed integer linear programming problem. It then searches for efficient solutions by relying on contract decompositions and a method based on sub graph isomorphism to iteratively prune infeasible architectures out of the search space. Experiments on a reconfigurable production line and an aircraft power distribution network show up to two orders of magnitude acceleration in architectural exploration with respect to comparable approaches.

Certificate functions can be used to efficiently capture and prove various properties of a system or controller. Control barrier functions (CBFs) are certificate functions that define a region of forward-invariance, which makes them a natural choice to enforce a notion of “safety” for a system. However, synthesizing CBFs, especially in the case of complex systems with learning-enabled components, remains a challenge. Recent work achieves promising results by leveraging neural networks as function approximators to learn CBFs. However, a single CBF may not exist or be difficult to obtain for complex hybrid systems. To overcome this difficulty, this paper presents a framework to simultaneously learn simpler, time-varying control barrier functions (TV-CBFs) that are composable. We embed these neural certificates in a compositional framework based on assume-guarantee contracts. The resulting neural barrier contracts can then be combined by leveraging the rigorous contract algebra. Learning multiple, composable CBFs empowers the verification process (1) by simplifying the verification of complex systems via decomposition and (2) by broadening the expressivity in capturing complex systems and controllers. We illustrate the effectiveness of our approach on the verification of an aircraft’s automatic landing system and a quadrotor navigating an indoor environment.

Graph neural networks (GNNs) have displayed significant potential in various graph-based learning tasks. However, the computational demands of deploying GNNs on large-scale graphs can grow exponentially. A recent method, termed unified graph sparsification (UGS), shows that there exists a pair consisting of a subgraph and a sparse subnetwork, called graph lottery ticket (GLT), that can effectively speed up GNN inference. However, despite their advantages, the performance of GLTs against adversarial structure perturbations remains largely unexplored. In this paper, we investigate the resilience of GLTs against different structure perturbation attacks under the poisoning attack setting. The evaluation results show that the GLTs identified by UGS are vulnerable and exhibit a large drop in classification accuracy for the adversarially perturbed graphs. We then propose a new technique for defending UGS that leverages self-training to find GLTs that are more resilient and can achieve better performance than plain UGS.

We present a methodology for scalable exploration of cyber-physical system architectures. We propose a mathematical formulation of the architecture exploration problem as an optimized mapping problem that includes joint selection of system topologies and components taken from predefined libraries. Using a graph-based representation of an architecture, we introduce novel compact encodings of mapping constraints and path constraints that significantly improve the scalability of the formulation. We use the new encodings to instantiate design requirements, such as interconnection, routing, timing, and energy constraints, on the architecture model. We implement our methods in an extensible architecture exploration toolbox, and provide a pattern-based language for formal, yet flexible, requirement specification. Numerical evaluations on a set of design problems from wireless sensor networks, reconfigurable manufacturing systems, and electrical power systems demonstrate the effectiveness of our approach.

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.

Logic locking is a promising technique for protecting integrated circuit designs while outsourcing their fabrication. Recently, graph neural network (GNN)-based link prediction attacks have been developed which can successfully break all the multiplexer-based locking techniques that were expected to be learning-resilient. We present SimLL, a novel similarity-based locking technique which locks a design using multiplexers and shows robustness against the existing structure-exploiting oracle-less learning-based attacks. Aiming to confuse the machine learning (ML) models, SimLL introduces key-controlled multiplexers between logic gates or wires that exhibit high levels of topological and functional similarity. Empirical results show that SimLL can degrade the accuracy of existing ML-based attacks to approximately 50%, resulting in a negligible advantage over random guessing.

We address the warehouse servicing problem (WSP) in automated warehouses, which use teams of mobile agents to bring products from shelves to packing stations. Given a list of products, the WSP amounts to finding a plan for a team of agents which brings every product on the list to a station within a given timeframe. The WSP consists of four subproblems, concerning what tasks to perform (task formulation), who will perform them (task allocation), and when (scheduling) and how (path planning) to perform them. These subproblems are NP-hard individually and are made more challenging by their interdependence. The difficulty of the WSP is compounded by the scale of automated warehouses, which frequently use teams of hundreds of agents. In this paper, we present a methodology that can solve the WSP at such scales. We introduce a novel, contract-based design framework which decomposes an automated warehouse into traffic system components. By assigning each of these components a contract describing the traffic flows it can support, we can syn-thesize a traffic flow satisfying a given WSP instance. Component-wise search-based path planning is then used to transform this traffic flow into a plan for discrete agents in a modular way. Evaluation shows that this methodology can solve WSP instances on real automated warehouses.

We address the Warehouse Servicing Problem (WSP) in automated warehouses, which use teams of mobile robots to move products from shelves to packaging stations. Given a list of products, the WSP amounts to finding a motion plan which brings every product on the list from a shelf to a packaging station within a given time limit. The WSP consists of four subproblems, namely, deciding where to source and deposit a product (task formulation), who should transport each product (task assignment) and when (scheduling) and how (motion planning). These problems are NP-Hard individually and made more challenging by their interdependence. The difficulty of the WSP is compounded by the scale of automated warehouses, which use teams of hundreds of agents to transport thousands of products. In this paper, we present Contract-based Cyclic Motion Planning (CCMP), a novel contract-based methodology for solving the WSP at scale. CCMP decomposes a warehouse into a set of traffic system components. By assigning each component a contract which describes the traffic flows it can support, CCMP can generate a traffic flow which satisfies a given WSP instance. CCMP then uses a novel motion planner to transform this traffic flow into a motion plan for a team of robots. Evaluation shows that CCMP can solve WSP instances taken from real industrial scenarios with up to 1 million products while outperforming other methodologies for solving the WSP by up to 2.9×.

The Boolean satisfiability (SAT) attack is an oracle-guided attack that can break most combinational logic locking schemes by efficiently pruning out all the wrong keys from the search space. Extending such an attack to sequential logic locking requires multiple time-consuming rounds of SAT solving, performed using an “unrolled” version of the sequential circuit, and model checking, used to determine the successful termination of the attack. This article addresses these challenges by formally characterizing the relation between the minimum unrolling depth required to prune out the wrong keys of an SAT-based attack and a notion of functional corruptibility (FC) for sequential circuits, which can be efficiently estimated from a locked circuit to indicate the progress of an SAT-based attack. Based on this analysis, we present an FC-guided SAT-based attack that can significantly reduce unnecessary SAT and model-checking tasks. We present two versions of the attack, namely,Fun-SATandFun-SAT+, based on whether the attacker has a priori knowledge of the key length.Fun-SATaims to find the correct key sequence, whileFun-SAT+aims to retrieve the correct initial state of the circuit. The numerical evaluation shows thatFun-SATcan be, on average,$90\boldsymbol {\times }$faster than previous attacks against state-of-the-art locking methods. On the other hand, when using an approximate termination condition,Fun-SAT+can find an initial state that leads to at most 0.1% FC in 76.9% instances that would otherwise time out after one day.

Sequential logic locking has been studied over the last decade as a method to protect sequential circuits from reverse engineering. However, most of the existing sequential logic locking techniques are threatened by increasingly more sophisticated SAT-based attacks, efficiently using input queries to a SAT solver to rule out incorrect keys, as well as removal attacks based on structural analysis. In this paper, we propose TriLock, a sequential logic locking method that simultaneously addresses these vulnerabilities. TriLock can achieve high, tunable functional corruptibility while still guaranteeing exponential queries to the SAT solver in a SAT-based attack. Further, it adopts a state re-encoding method to obscure the boundary between the original state registers and those inserted by the locking method, thus making it more difficult to detect and remove the locking-related components.

This paper proposes an automated framework for quantitative verification and design space exploration of cyber-physical systems in the presence of uncertainty, leveraging assume-guarantee contracts expressed in Stochastic Signal Temporal Logic (StSTL). We introduce quantitative semantics for StSTL and formulations of the quantitative verification and design space exploration problems as bi-level optimization problems. We show that these optimization problems can be effectively solved for a class of stochastic systems and a fragment of bounded-time StSTL formulas. Our algorithm searches for partitions of the upper-level design space such that the solutions of the lower-level problems satisfy the upper-level constraints. A set of optimal parameter values are then selected within these partitions. We illustrate the effectiveness of our framework on the design of a multi-sensor perception system and an automatic cruise control system.

Autonomous agents often operate in environments where the state is partially observed. In addition to maximizing their cumulative reward, agents must execute complex tasks with rich temporal and logical structures. These tasks can be expressed using temporal logic languages like finite linear temporal logic. This paper, for the first time, provides a structured framework for designing agent policies that maximize the reward while ensuring that the probability of satisfying the temporal logic specification is sufficiently high. We reformulate the problem as a constrained partially observable Markov decision process (POMDP) and provide a novel approach that can leverage off-the-shelf unconstrained POMDP solvers for solving it. Our approach guarantees approximate optimality and constraint satisfaction with high probability. We demonstrate its effectiveness by implementing it on several models of interest.

Constrained Markov decision processes (CMDPs) formalize sequential decision-making problems whose objective is to minimize a cost function while satisfying constraints on various cost functions. In this paper, we consider the setting of episodic fixed-horizon CMDPs. We propose an online algorithm which leverages the linear programming formulation of repeated optimistic planning for finite-horizon CMDP to provide a probably approximately correctness (PAC) guarantee on the number of episodes needed to ensure a near optimal policy, i.e., with resulting objective value close to that of the optimal value and satisfying the constraints within low tolerance, with high probability. The number of episodes needed is shown to have linear dependence on the sizes of the state and action spaces and quadratic dependence on the time horizon and an upper bound on the number of possible successor states for a state-action pair. Therefore, if the upper bound on the number of possible successor states is much smaller than the size of the state space, the number of needed episodes becomes linear in the sizes of the state and action spaces and quadratic in the time horizon.

We introduce a systematic framework for logic locking of integrated circuits based on the analysis of the sources of information leakage from both the circuit and the locking scheme and their formalization into a notion of risk that can guide the design against existing and possible future attacks. We further propose a two-level optimization-based methodology to generate locking strategies minimizing a cost function and balancing security, risk, and implementation overhead, out of a collection of locking primitives. Optimization results on a set of case studies show the potential of layering multiple locking primitives to provide high security at significantly lower risk.

Reverse engineering an integrated circuit netlist is a powerful tool to help detect malicious logic and counteract design piracy. A critical challenge in this domain is the correct classification of data-path and control-logic registers in a design. We present ReIGNN, a novel learning-based register classification methodology that combines graph neural networks (GNNs) with structural analysis to classify the registers in a circuit with high accuracy and generalize well across different designs. GNNs are particularly effective in processing circuit netlists in terms of graphs and leveraging properties of the nodes and their neighborhoods to learn to efficiently discriminate between different types of nodes. Structural analysis can further rectify any registers misclassified as state registers by the GNN by analyzing strongly connected components in the netlist graph. Numerical results on a set of benchmarks show that ReIGNN can achieve, on average, 96.5% balanced accuracy and 97.7% sensitivity across different designs.

Logic locking is a well-explored defense mechanism against various types of hardware security attacks. Recent approaches to logic locking replace portions of a circuit with reconfigurable blocks such as look-up tables (LUTs) and switch boxes (SBs) to primarily achieve logic and routing obfuscation, respectively. However, these techniques may incur significant design overhead, and methods that can mitigate the implementation cost for a given security level are desirable. In this paper, we address this challenge by proposing an algorithm for deciding the location and inputs of the LUTs in LUT-based obfuscation to enhance security and reduce design overhead. We then introduce a locking method that combines LUTs with SBs to further robustify LUT-based obfuscation, largely independently of the specific LUT locations. We illustrate the effectiveness of the proposed approaches on a set of ISCAS benchmark circuits.

We address the problem of automatically constructing a formal robotic mission specification in a logic language with precise semantics starting from an informal description of the mission requirements. We present CROME (Contract-based RObotic Mission spEcification), a framework that allows capturing mission requirements in terms of goals by using specification patterns, and automatically building linear temporal logic mission specifications conforming with the requirements. CROME leverages a new formal model, termed Contract-based Goal Graph (CGG), which enables organizing the requirements in a modular way with a rigorous compositional semantics. By relying on the CGG, it is then possible to automatically: i) check the feasibility of the overall mission, ii) further refine it from a library of pre-defined goals, and iii) synthesize multiple controllers that implement different parts of the mission at different abstraction levels, when the specification is realizable. If the overall mission is not realizable, CROME identifies mission scenarios, i.e., sub-missions that can be realizable. We illustrate the effectiveness of our methodology and supporting tool on a case study.

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.

We propose SANSCrypt, a novel sequential logic encryption scheme to protect integrated circuits against reverse engineering. Previous sequential encryption methods focus on modifying the circuit state machine such that the correct functionality can be accessed by applying the correct key sequence only once. Considering the risk associated with one-time authentication, SANSCrypt adopts a new temporal dimension to logic encryption, by requiring the user to sporadically perform multiple authentications according to a protocol based on pseudorandom number generation. Analysis and validation results on a set of benchmark circuits show that SANSCrypt offers a substantial output corruptibility if the key sequences are applied incorrectly. Moreover, it exhibits an exponential resilience to existing attacks, including SAT-based attacks, while maintaining a reasonably low overhead.

We address the problem of synthesizing safety-critical embedded and cyber-physical system architectures to minimize a cost function while guaranteeing the desired reliability. We represent a system architecture as a configurable graph in which both the nodes (components) and edges (interconnections) may fail. We then propose a compact analytical formalism to efficiently reason about the reliability of the overall system based on the failure probabilities of the components, and provide expressions of the design constraints that avoid exhaustive enumeration of failure cases on all possible graph configurations. Based on these constraints, we cast the synthesis problem as an optimization problem and propose monolithic and iterative optimization schemes to decrease the problem complexity. We implement the proposed algorithms in the ArchEx framework, leveraging a pattern-based specification language to facilitate problem formulation. Design problems from aircraft electric power distribution networks and reconfigurable industrial manufacturing systems illustrate the effectiveness of our approach.

Efficiently recognizing the functionality of a circuit is key to many applications, such as formal verification, reverse engineering, and security. We present a scalable framework for gate-level circuit recognition that leverages deep learning and a convolutional neural network (CNN)-based circuit representation. Given a standard cell library, we present a sparse mapping algorithm to improve the time and memory efficiency of the CNN-based circuit representation. Sparse mapping allows encoding only the logic cell functionality, independently of implementation parameters such as timing or area. We further propose a data structure, termed level-dependent decaying sum (LDDS) existence vector, which can compactly represent information about the circuit topology. Given a reference gate in the circuit, an LDDS vector can capture the function of the gates in the input and output cones as well as their distance (number of stages) from the reference. Compared to the baseline approach, our framework obtains more than an-order-of-magnitude reduction in the average training time and 2× improvement in the average runtime for generating CNN-based representations from gate-level circuits, while achieving 10% higher accuracy on a set of benchmarks including EPFL and ISCAS'85 circuits.

Assume-guarantee (A/G) contracts are mathematical models enabling modular and hierarchical design and verifi-cation of complex systems by rigorous decomposition of system-level specifications into component-level specifications. Existing A/G contract frameworks, however, are not designed to effectively capture the behaviors of cyber-physical systems where multiple agents aim to maximize one or more objectives, and may interact with each other and the environment in a cooperative or non-cooperative way toward achieving their goals. We propose an extension of the A/G contract framework, namely optimizing A/G contracts, that can be used to specify and reason about properties of component interactions that involve optimizing objectives. The proposed framework includes methods for constructing new contracts via conjunction and composition, along with algorithms to verify system properties via contract refinement. We illustrate its effectiveness on a set of case studies from connected and autonomous vehicles.

We propose an efficient multi-robot motion planning algorithm for missions captured by linear temporal logic (LTL) specifications, in the presence of bounded disturbances and denial-of-service (DoS) attacks against the communication between robots and base stations. Given an LTL formula Ψ, our goal is to construct robot trajectories, and associated control strategies, to satisfy Ψ and continuously establish communication paths between robots and base stations despite the DoS attacks and the disturbances on the robot states. Our approach combines and extends results from robust control and efficient motion planning via satisfiability modulo convex programming (SMC). We first compute a feedback controller that rejects the disturbance together with a perturbation of the DoS-free workspace that accounts for the worst-case disturbance scenario. On the perturbed workspace, we formulate the planning problem as a feasibility problem over Boolean and convex constraints, respectively capturing the DoS-resilient mission constraints and the constraints on the nominal, disturbance-free, robot dynamics. Numerical results show the effectiveness of our algorithm in providing DoS-resilient plans that are robust to disturbances and support the execution of complex missions.

This talk discusses some of the design challenges posed by cyber-physical system security at different abstraction layers, from algorithm design to the realization of trusted hardware platforms. We introduce two design problems, namely, detecting sensor attacks in large-scale cyber-physical systems, and systematic design of circuit obfuscation schemes to satisfy system-level security requirements. We then summarize some of the approaches pursued by the research community to address these problems, with the potential of fostering new methodologies, algorithms, and tools for the design of secure and trustworthy cyber-physical systems.

This paper reflects on the design challenges posed by cyber-physical systems, what distinguishes cyber-physical system design from large-scale integrated circuit design, and what could be the opportunities for the design automation community. The paper discusses three challenges that touch upon aspects that are unique to cyber-physical systems, namely, devising novel compositional design methodologies, reasoning about the interaction between discrete and continuous models, and dealing with uncertainty. It then summarizes some of the approaches pursued by the research community to tackle these challenges, with the potential of fostering a new generation of methodologies, algorithms, and tools for system design. Central to the paper is a view of platforms and contracts as formal notions that can bridge the emerging area of cyber-physical system design automation with paradigms that have been successful in the field of electronic design automation.

Research in logic encryption over the last decade has resulted in various techniques to prevent different security threats such as Trojan insertion, intellectual property leakage, and reverse engineering. However, there is little agreement on a uniform set of metrics and models to efficiently assess the achieved security level and the trade-offs between security and overhead. This paper addresses the above challenges by relying on a general logic encryption model that can encompass all the existing techniques, and a uniform set of metrics that can capture multiple, possibly conflicting, security concerns. We apply our modeling approach to four state-of-the-art encryption techniques, showing that it enables fast and accurate evaluation of design trade-offs, average prediction errors that are at least 2× smaller than previous approaches, and the evaluation of compound encryption methods.

We present an assume-guarantee contract framework for cyber-physical system design under probabilistic requirements. Given a stochastic linear system and a set of requirements captured by bounded Stochastic Signal Temporal Logic (StSTL) contracts, we propose algorithms to check contract compatibility, consistency, and refinement, and generate a sequence of control inputs that satisfies a contract. We leverage encodings of the verification and control synthesis tasks into mixed integer optimization problems, and conservative approximations of probabilistic constraints that produce sound and tractable problem formulations. We illustrate the effectiveness of our approach on three case studies, including the design of controllers for aircraft power distribution networks.

We address the design space exploration of wireless networks to jointly select topology and component sizing. We formulate the exploration problem as an optimized mapping problem, where network elements are associated with components from pre-defined libraries to minimize a cost function under correctness guarantees. We express a rich set of system requirements as mixed integer linear constraints over path variables, denoting the presence or absence of paths between network nodes, and propose an algorithm for efficient, compact encoding of feasible paths that can reduce by orders of magnitude the complexity of the optimization problem. We incorporate our methods in a system-level design space exploration toolbox and evaluate their effectiveness on design examples from data collection and localization networks.

This paper presents CHASE, a framework for requirement capture, formalization, and validation for cyber-physical systems. CHASE combines a practical front-end formal specification language based on patterns with a rigorous verification back-end based on assume-guarantee contracts. The front-end language can express temporal properties of networks using a declarative style, and supports automatic translation from natural-language constructs to low-level mathematical languages. The verification back-end leverages the mathematical formalism of contracts to reason about system requirements and determine inconsistencies and dependencies between them. CHASE features a modular and extensible software infrastructure that can support different domain-specific languages, modeling formalisms, and analysis tools. We illustrate its effectiveness on industrial design examples, including control of aircraft power distribution networks and arbitration of a mixed-criticality automotive bus.

Smart buildings today are aimed at providing safe, healthy, comfortable, affordable, and beautiful spaces in a carbon and energy-efficient way. They are emerging as complex cyber-physical systems with humans in the loop. Cost, the need to cope with increasing functional complexity, flexibility, fragmentation of the supply chain, and time-to-market pressure are rendering the traditional heuristic and ad hoc design paradigms inefficient and insufficient for the future. In this paper, we present a platform-based methodology for smart building design. Platform-based design (PBD) promotes the reuse of hardware and software on shared infrastructures, enables rapid prototyping of applications, and involves extensive exploration of the design space to optimize design performance. In this paper, we identify, abstract, and formalize components of smart buildings, and present a design flow that maps high-level specifications of desired building applications to their physical implementations under the PBD framework. A case study on the design of on-demand heating, ventilation, and air conditioning (HVAC) systems is presented to demonstrate the use of PBD.

The design of cyber-physical systems (CPSs) requires methods and tools that can efficiently reason about the interaction between discrete models, e.g., representing the behaviors of “cyber” components, and continuous models of physical processes. Boolean methods such as satisfiability (SAT) solving are successful in tackling large combinatorial search problems for the design and verification of hardware and software components. On the other hand, problems in control, communications, signal processing, and machine learning often rely on convex programming as a powerful solution engine. However, despite their strengths, neither approach would work in isolation for CPSs. In this paper, we present a new satisfiability modulo convex programming (SMC) framework that integrates SAT solving and convex optimization to efficiently reason about Boolean and convex constraints at the same time. We exploit the properties of a class of logic formulas over Boolean and nonlinear real predicates, termed monotone satisfiability modulo convex formulas, whose satisfiability can be checked via a finite number of convex programs. Following the lazy satisfiability modulo theory (SMT) paradigm, we develop a new decision procedure for monotone SMC formulas, which coordinates SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. A key step in our coordination scheme is the efficient generation of succinct infeasibility proofs for inconsistent constraints that can support conflict-driven learning and accelerate the search. We demonstrate our approach on different CPS design problems, including spacecraft docking mission control, robotic motion planning, and secure state estimation. We show that SMC can handle more complex problem instances than state-of-the-art alternative techniques based on SMT solving and mixed integer convex programming.

We introduce a scalable observer architecture, which can efficiently estimate the states of a discrete-time linear-time-invariant system whose sensors are manipulated by an attacker, and is robust to measurement noise. Given an upper bound on the number of attacked sensors, we build on previous results on necessary and sufficient conditions for state estimation, and propose a novel Multi-Modal Luenberger (MML) observer based on efficient Satisfiability Modulo Theory (SMT) solving. We present two techniques to reduce the complexity of the estimation problem. As a first strategy, instead of a bank of distinct observers, we use a family of filters sharing a single dynamical equation for the states, but different output equations, to generate estimates corresponding to different subsets of sensors. Such an architecture can reduce the memory usage of the observer from an exponential to a linear function of the number of sensors. We then develop an efficient SMT-based decision procedure that is able to reason about the estimates of the MML observer to detect at runtime which sets of sensors are attack-free, and use them to obtain a correct state estimate. Finally, we discuss two optimization-based algorithms that can efficiently select the observer parameters with the goal of minimizing the sensitivity of the estimates with respect to sensor noise. We provide proofs of convergence for our estimation algorithm and report simulation results to compare its runtime performance with alternative techniques. We show that our algorithm scales well for large systems (including up to 5,000 sensors) for which many previously proposed algorithms are not implementable due to excessive memory and time requirements. Finally, we illustrate the effectiveness of our approach, both in terms of resiliency to attacks and robustness to noise, on the design of large-scale power distribution networks.

We present ArchEx, a framework for cyber-physical system architecture exploration. We formulate the exploration problem as a mapping problem, where "virtual" components are mapped into "real" components from pre-defined libraries to minimize an objective function while guaranteeing that system requirements are satisfied. ArchEx leverages an extensible set of patterns to enable formal, yet flexible, requirement specification, a graph-based internal representation of the system architecture, and algorithms based on mixed integer linear programming to solve the mapping problem. Its effectiveness is demonstrated on two industrial case studies: an aircraft power distribution network and a reconfigurable automated production line.

We address the design space exploration of wireless body area networks for wearable and implantable technologies, a task that is increasingly challenging as the number and variety of devices per person grow. Our method efficiently decomposes the problem into smaller subproblems by coordinating specialized analysis and optimization techniques. We leverage mixed integer linear programming to generate candidate network configurations based on coarse energy estimations. Accurate discrete-event simulation is used to check the feasibility of the proposed configurations under reliability constraints and guide the search to achieve fast convergence. Numerical results show that our application-specific approach substantially reduces the exploration time with respect to generic optimization techniques and helps provide clear identification of promising solutions.

We address the problem of determining the satisfiability of a Boolean combination of convex constraints over the real numbers, which is common in the context of hybrid system verification and control. We first show that a special type of logic formulas, termed monotone Satisfiability Modulo Convex (SMC) formulas, is the most general class of formulas over Boolean and nonlinear real predicates that reduce to convex programs for any satisfying assignment of the Boolean variables. For this class of formulas, we develop a new satisfiability modulo convex optimization procedure that uses a lazy combination of SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. Our approach can then leverage the efficiency and the formal guarantees of state-of-the-art algorithms in both the Boolean and convex analysis domains. A key step in lazy satisfiability solving is the generation of succinct infeasibility proofs that can support conflict-driven learning and decrease the number of iterations between the SAT and the theory solver. For this purpose, we propose a suite of algorithms that can trade complexity with the minimality of the generated infeasibility certificates. Remarkably, we show that a minimal infeasibility certificate can be generated by simply solving one convex program for a sub-class of SMC formulas, namely ordered positive unate SMC formulas, that have additional monotonicity properties. Perhaps surprisingly, ordered positive unate formulas appear themselves very frequently in a variety of practical applications. By exploiting the properties of monotone SMC formulas, we can then build and demonstrate effective and scalable decision procedures for problems in hybrid system verification and control, including secure state estimation and robotic motion planning.

We develop an assume-guarantee contract framework for the design of cyber-physical systems, modeled as closed-loop control systems, under probabilistic requirements. We use a variant of signal temporal logic, namely, Stochastic Signal Temporal Logic (StSTL) to specify system behaviors as well as contract assumptions and guarantees, thus enabling automatic reasoning about requirements of stochastic systems. Given a stochastic linear system representation and a set of requirements captured by bounded StSTL contracts, we propose algorithms that can check contract compatibility, consistency, and refinement, and generate a controller to guarantee that a contract is satisfied, following a stochastic model predictive control approach. Our algorithms leverage encodings of the verification and control synthesis tasks into mixed integer optimization problems, and conservative approximations of probabilistic constraints that produce both sound and tractable problem formulations. We illustrate the effectiveness of our approach on a few examples, including the design of embedded controllers for aircraft power distribution networks.

We address the problem of diagnosing and repairing specifications for hybrid systems, formalized in signal temporal logic (STL). Our focus is on automatic synthesis of controllers from specifications using model predictive control. We build on recent approaches that reduce the controller synthesis problem to solving one or more mixed integer linear programs (MILPs), where infeasibility of an MILP usually indicates unrealizability of the controller synthesis problem. Given an infeasible STL synthesis problem, we present algorithms that provide feedback on the reasons for unrealizability, and suggestions for making it realizable. Our algorithms are sound and complete relative to the synthesis algorithm, i.e., they provide a diagnosis that makes the synthesis problem infeasible, and always terminate with a non-trivial specification that is feasible using the chosen synthesis method, when such a solution exists. We demonstrate the effectiveness of our approach on controller synthesis for various cyber-physical systems, including an autonomous driving application and an aircraft electric power system.

We propose a methodology for architecture exploration for Cyber-Physical Systems (CPS) based on an iterative, optimization-based approach, where a discrete architecture selection engine is placed in a loop with a continuous sizing engine. The discrete optimization routine proposes a candidate architecture to the sizing engine. The sizing routine optimizes over the continuous parameters using simulation to evaluate the physical models and to monitor the requirements. To decrease the number of simulations, we show how balance equations and conservation laws can be leveraged to prune the discrete space, thus achieving significant reduction in the overall runtime. We demonstrate the effectiveness of our methodology on an industrial case study, namely an aircraft environmental control system, showing more than one order of magnitude reduction in optimization time.

We introduce a platform-based design methodology that uses contracts to specify and abstract the components of a cyber-physical system (CPS), and provide formal support to the entire CPS design flow. The design is carried out as a sequence of refinement steps from a high-level specification to an implementation built out of a library of components at the lower level. We review formalisms and tools that can be used to specify, analyze, or synthesize the design at different levels of abstraction. For each level, we highlight how the contract operations can be concretely computed as well as the research challenges that should be faced to fully implement them. We illustrate our approach on the design of embedded controllers for aircraft electric power distribution systems.

Given a global specification contract and a system described by a composition of contracts, system verification reduces to checking that the composite contract refines the specification contract, i.e. that any implementation of the composite contract implements the specification contract and is able to operate in any environment admitted by it. Contracts are captured using high-level declarative languages, for example, linear temporal logic (LTL). In this case, refinement checking reduces to an LTL satisfiability checking problem, which can be very expensive to solve for large composite contracts. This paper proposes a scalable refinement checking approach that relies on a library of contracts and local refinement assertions. We propose an algorithm that, given such a library, breaks down the refinement checking problem into multiple successive refinement checks, each of smaller scale. We illustrate the benefits of the approach on an industrial case study of an aircraft electric power system, with up to two orders of magnitude improvement in terms of execution time.

We introduce a platform-based design methodology that addresses the complexity and heterogeneity of cyber-physical systems by using assume-guarantee contracts to formalize the design process and enable realization of control protocols in a hierarchical and compositional manner. Given the architecture of the physical plant to be controlled, the design is carried out as a sequence of refinement steps from an initial specification to a final implementation, including synthesis from requirements and mapping of higher-level functional and nonfunctional models into a set of candidate solutions built out of a library of components at the lower level. Initial top-level requirements are captured as contracts and expressed using linear temporal logic (LTL) and signal temporal logic (STL) formulas to enable requirement analysis and early detection of inconsistencies. Requirements are then refined into a controller architecture by combining reactive synthesis steps from LTL specifications with simulation-based design space exploration steps. We demonstrate our approach on the design of embedded controllers for aircraft electric power distribution.

Contract-based design is emerging as a unifying compositional paradigm for the specification, design and verification of large-scale complex systems. Different contract frameworks are currently available, but we lack a clear understanding of the relations between them. In this paper, we investigate the relation between interface theories (specifically, relational interfaces) and assume-guarantee (A/G) contracts. We introduce a natural transformation of interfaces to A/G contracts represented by linear temporal logic. Then, we analyze differences and correspondences between key operators and relations in the two theories (i.e. composition, refinement and conjunction), by studying their preservation properties under the proposed transformation. We show that the transformation preserves refinement, but does not generally preserve serial composition and conjunction. Then, we present an assumption-projection operator to make it possible to preserve serial composition and compatibility checking. Finally, we provide illustrative examples that shed light on the effectiveness of both frameworks for requirement formalization, early detection of integration errors, and use of abstraction-refinement.

Efficient system-level design is increasingly relying on hierarchical design-space exploration, as well as compositional methods, to shorten time-to-market, leverage design re-use, and achieve optimal performances. However, in analog electronic systems, circuit behaviors are so tightly dependent on their interface conditions that accurate system performance estimations based on characterizations of individual stand-alone circuits is a hard task. Since there is no general solution to this problem, analog system integration has traditionally used ad-hoc solutions heavily dependent on designers' experience. In this paper, we build upon the analog platform-based design methodology by exploiting contracts to enforce correct-by-construction system-level composition. Contracts intuitively capture the thought process of a designer, who aims at guaranteeing circuit performance only under specific assumptions (e.g. loading and dynamic range) on the interface properties. Our approach allows automatic detection and composition of compatible components in a given library. We apply our methodology to an ultra-wide band receiver front-end to show that contracts allow pre-designed IP components to be smoothly integrated and design decisions to be reliably made at a higher abstraction level, both key factors to improve designer productivity.