-
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 map**s 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 map**s 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.
