Showing 1–7 of 7 results for author: Incer, I

A Compositional Approach to Diagnosing Faults in Cyber-Physical Systems

Authors: Josefine B. Graebener, Inigo Incer, Richard M. Murray

Abstract: Identifying the cause of a system-level failure in a cyber-physical system (CPS) can be like tracing a needle in a haystack. This paper approaches the problem by assuming that the CPS has been designed compositionally and that each component in the system is associated with an assume-guarantee contract. We exploit recent advances in contract-based design that show how to compute the contract for t… ▽ More Identifying the cause of a system-level failure in a cyber-physical system (CPS) can be like tracing a needle in a haystack. This paper approaches the problem by assuming that the CPS has been designed compositionally and that each component in the system is associated with an assume-guarantee contract. We exploit recent advances in contract-based design that show how to compute the contract for the entire system using the component-level contracts. When presented with a system-level failure, our approach is able to efficiently identify the components that are responsible for the system-level failure together with the specific predicates in those components' specifications that are involved in the fault. We implemented this approach using Pacti and demonstrate it through illustrative examples inspired by an autonomous vehicle in the DARPA urban challenge. △ Less

Submitted 7 July, 2025; originally announced July 2025.

Early Design Exploration of Aerospace Systems Using Assume-Guarantee Contracts

Authors: Nicolas Rouquette, Alessandro Pinto, Inigo Incer

Abstract: We present a compositional approach to early modeling and analysis of complex aerospace systems based on assume-guarantee contracts. Components in a system are abstracted into assume-guarantee specifications. Performing algebraic contract operations with Pacti allows us to relate local component specifications to that of the system. Applications to two aerospace case studies (the design of spacecr… ▽ More We present a compositional approach to early modeling and analysis of complex aerospace systems based on assume-guarantee contracts. Components in a system are abstracted into assume-guarantee specifications. Performing algebraic contract operations with Pacti allows us to relate local component specifications to that of the system. Applications to two aerospace case studies (the design of spacecraft to satisfy a rendezvous mission and the design of the thermal management system of a prototypical aircraft) show that this methodology provides engineers with an agile, early analysis and exploration process. △ Less

Submitted 3 September, 2024; originally announced September 2024.

Comments: 32 pages

Composition and Merging of Assume-Guarantee Contracts Are Tensor Products

Authors: Inigo Incer

Abstract: We show that the operations of composition and merging of contracts are part of the tensor product structure of the algebra of contracts. We show that the operations of composition and merging of contracts are part of the tensor product structure of the algebra of contracts. △ Less

Submitted 9 May, 2024; originally announced May 2024.

Specifying and Analyzing Networked and Layered Control Systems Operating on Multiple Clocks

Authors: Inigo Incer, Noel Csomay-Shanklin, Aaron Ames, Richard M. Murray

Abstract: We consider the problem of reasoning about networked and layered control systems using assume-guarantee specifications. As these systems are formed by the interconnection of components that operate under various clocks, we introduce a new logic, Multiclock Logic (MCL), to be able to express the requirements of components form the point of view of their local clocks. Specifying components locally p… ▽ More We consider the problem of reasoning about networked and layered control systems using assume-guarantee specifications. As these systems are formed by the interconnection of components that operate under various clocks, we introduce a new logic, Multiclock Logic (MCL), to be able to express the requirements of components form the point of view of their local clocks. Specifying components locally promotes independent design and component reuse. We carry out a contract-based analysis of a control system implemented via two control algorithms (model predictive control and feedback linearization) running on their own processors and clocks. Then we implement each of the contracts to build a system. The system performs as desired when the requirements derived from our system-level analysis are respected. Violating the constraints required by the contract-based analysis of the system leads to error. △ Less

Submitted 18 February, 2024; originally announced February 2024.

Some Algebraic Aspects of Assume-Guarantee Reasoning

Authors: Inigo Incer, Albert Benveniste, Alberto Sangiovanni-Vincentelli

Abstract: We present the algebra of assume-guarantee (AG) contracts. We define contracts, provide new as well as known operations, and show how these operations are related. Contracts are functorial: any Boolean algebra has an associated contract algebra. We study monoid and semiring structures in contract algebra -- and the mappings between such structures. We discuss the actions of a Boolean algebra on it… ▽ More We present the algebra of assume-guarantee (AG) contracts. We define contracts, provide new as well as known operations, and show how these operations are related. Contracts are functorial: any Boolean algebra has an associated contract algebra. We study monoid and semiring structures in contract algebra -- and the mappings between such structures. We discuss the actions of a Boolean algebra on its contract algebra. △ Less

Submitted 16 September, 2023; originally announced September 2023.

Context-Aided Variable Elimination for Requirement Engineering

Authors: Inigo Incer, Albert Benveniste, Richard M. Murray, Alberto Sangiovanni-Vincentelli, Sanjit A. Seshia

Abstract: Deriving system-level specifications from component specifications usually involves the elimination of variables that are not part of the interface of the top-level system. This paper presents algorithms for eliminating variables from formulas by computing refinements or relaxations of these formulas in a context. We discuss a connection between this problem and optimization and give efficient alg… ▽ More Deriving system-level specifications from component specifications usually involves the elimination of variables that are not part of the interface of the top-level system. This paper presents algorithms for eliminating variables from formulas by computing refinements or relaxations of these formulas in a context. We discuss a connection between this problem and optimization and give efficient algorithms to compute refinements and relaxations of linear inequality constraints. △ Less

Submitted 27 May, 2023; originally announced May 2023.

Pacti: Scaling Assume-Guarantee Reasoning for System Analysis and Design

Authors: Inigo Incer, Apurva Badithela, Josefine Graebener, Piergiuseppe Mallozzi, Ayush Pandey, Sheng-Jung Yu, Albert Benveniste, Benoit Caillaud, Richard M. Murray, Alberto Sangiovanni-Vincentelli, Sanjit A. Seshia

Abstract: Contract-based design is a method to facilitate modular system design. While there has been substantial progress on the theory of contracts, there has been less progress on scalable algorithms for the algebraic operations in this theory. In this paper, we present: 1) principles to implement a contract-based design tool at scale and 2) Pacti, a tool that can efficiently compute these operations. We… ▽ More Contract-based design is a method to facilitate modular system design. While there has been substantial progress on the theory of contracts, there has been less progress on scalable algorithms for the algebraic operations in this theory. In this paper, we present: 1) principles to implement a contract-based design tool at scale and 2) Pacti, a tool that can efficiently compute these operations. We then illustrate the use of Pacti in a variety of case studies. △ Less

Submitted 30 March, 2023; originally announced March 2023.