CaltechAUTHORS
Published January 2025 | Version Published
Journal Article Open

Pacti: Assume-Guarantee Contracts for Efficient Compositional Analysis and Design

Creators

  • 1. ROR icon University of Michigan–Ann Arbor
  • 2. ROR icon Princeton University
  • 3. ROR icon California Institute of Technology
  • 4. ROR icon University of California, Berkeley
  • 5. ROR icon University of California, Merced
  • 6. ROR icon Jet Propulsion Lab
  • 7. INRIA/IRISA Rennes, France

Abstract

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 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 illustrate the use of Pacti in a variety of case studies.

Copyright and License

© 2025 Copyright held by the owner/author(s). Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of the United States government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

Funding

During the completion of this work, I. Incer was with the California Institute of Technology and the University of California, Berkeley; A. Badithela and A. Pandey were with the California Institute of Technology. This work was supported by NSF and ASEE through an eFellows postdoctoral fellowship, the DARPA LOGiCS project under contract FA8750-20-C-0156, the Air Force Office of Scientific Research (AFOSR) under MURI grant FA9550-22-1-0316 and grant FA9550-22-1-0333, Toyota under the iCyPhy Center at UC Berkeley, and the Wallenberg AI Autonomous Systems and Software Program (WASP).

Files

3704736.pdf

Files (6.6 MB)

Name Size
md5:a1ef121bbaad0bf716f0c211128f14bf
6.6 MB Preview Download

Additional details

Funding

National Science Foundation
American Society For Engineering Education
DARPA LOGiCS project FA8750-20-C-0156
United States Air Force Office of Scientific Research
MURI FA9550-22-1-0316
United States Air Force Office of Scientific Research
MURI FA9550-22-1-0333

Dates

Accepted
2024-10-26
Accepted
Available
2024-11-18
Published online AM
Available
2025-01-13
Published online

Caltech Custom Metadata

Publication Status
Published