Pacti: Assume-Guarantee Contracts for Efficient Compositional Analysis and Design
Contract-based design is a method to facilitate modular design of systems. While there has been substantial progress on the theory of contracts, there has been less progress on practical algorithms for the algebraic operations in the theory. In this article, 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 illustrate the use of Pacti in a variety of case studies.
Authors
- Sheng-Jung Yu (ORCID: https://orcid.org/0000-0003-2585-9586)
- Josefine B. Graebener (ORCID: https://orcid.org/0000-0002-1376-0741)
- Inigo Incer (ORCID: https://orcid.org/0000-0001-7933-692X)
- Benoı̂t Caillaud (ORCID: https://orcid.org/0000-0002-3234-5033)
- Apurva Badithela (ORCID: https://orcid.org/0000-0002-9788-2702)
- Piergiuseppe Mallozzi (ORCID: https://orcid.org/0000-0002-4438-6107)
- Sanjit A. Seshia (ORCID: https://orcid.org/0000-0001-6190-8707)
- Richard M. Murray (ORCID: https://orcid.org/0000-0002-5785-7481)
- Albert Benveniste (ORCID: https://orcid.org/0000-0003-3352-4137)
- Ayush Pandey (ORCID: https://orcid.org/0000-0003-3590-4459)
- Alberto Sangiovanni‐Vincentelli (ORCID: https://orcid.org/0000-0003-1298-8389)
- Nicolas Rouquette (ORCID: https://orcid.org/0000-0003-3137-8690)
Institutions
- California Institute of Technology (US)
- Institut national de recherche en sciences et technologies du numérique (FR)
- Jet Propulsion Laboratory (US)
- University of California, Merced (US)
- Princeton University (US)
- University of Michigan (US)
- Institut de Recherche en Informatique et Systèmes Aléatoires (FR)
- Université Bourgogne Franche-Comté (FR)
- University of California, Berkeley (US)
Publication Details
- Journal
- ACM Transactions on Cyber-Physical Systems
- Published
- 2024-11-18
- DOI
- https://doi.org/10.1145/3704736
- Citations
- 5
- Primary Topic
- Formal Methods in Verification
- Type
- article
- Field-Weighted Citation Impact
- 1.81
Funders
- Air Force Office of Scientific Research