Sheng-Jung Yu

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2024-238

December 27, 2024

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2024/EECS-2024-238.pdf

Complexity and heterogeneity are fundamental challenges for system design, as they prolong the design process and increase its cost. Independent design is a promising design flow to address these challenges whereby a supplier can develop its component without exchanging system-level information with other suppliers. Recent research on assume-guarantee contracts and contract-based design has focused on algebraic concepts, such as refinement and composition, to achieve independent design. However, the conventional definition of assume-guarantee contracts may result in implementations that may not operate correctly in the targeted environment of the system, thus hindering independent design. In this report, we introduce the concept of contract replaceability, a binary relation on contracts that prevents this problem. We then extend the requirements to include receptiveness as a constraint on assume-guarantee contracts to ensure strong replaceability. The properties derived from the constraints ensure that strong replaceability is satisfied under contract refinement and cascade composition. Thus any assume-guarantee contract that satisfies this constraint permits independent design.

Advisors: Alberto L. Sangiovanni-Vincentelli

---

BibTeX citation:

@mastersthesis{Yu:EECS-2024-238,
    Author= {Yu, Sheng-Jung},
    Title= {Contract Replaceability for Ensuring Independent Design using Assume-Guarantee Contracts},
    School= {EECS Department, University of California, Berkeley},
    Year= {2024},
    Month= {Dec},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2024/EECS-2024-238.html},
    Number= {UCB/EECS-2024-238},
    Abstract= {Complexity and heterogeneity are fundamental challenges for system design, as they prolong the design process and increase its cost. Independent design is a promising design flow to address these challenges whereby a supplier can develop its component without exchanging system-level information with other suppliers.
Recent research on assume-guarantee contracts and contract-based design has focused on algebraic concepts, such as refinement and composition, to achieve independent design.
However, the conventional definition of assume-guarantee contracts may result in implementations that may not operate correctly in the targeted environment of the system, thus hindering independent design.
In this report, we introduce the concept of contract replaceability, a binary relation on contracts that prevents this problem.
We then extend the requirements to include receptiveness as a constraint on assume-guarantee contracts to ensure strong replaceability.
The properties derived from the constraints ensure that strong replaceability is satisfied under contract refinement and cascade composition. 
Thus any assume-guarantee contract that satisfies this constraint permits independent design.},
}

EndNote citation:

%0 Thesis
%A Yu, Sheng-Jung 
%T Contract Replaceability for Ensuring Independent Design using Assume-Guarantee Contracts
%I EECS Department, University of California, Berkeley
%D 2024
%8 December 27
%@ UCB/EECS-2024-238
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2024/EECS-2024-238.html
%F Yu:EECS-2024-238