Automating Contract-based Design for Cyber-Physical Systems
Sheng-Jung Yu
EECS Department, University of California, Berkeley
Technical Report No. UCB/EECS-2025-84
May 16, 2025
http://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-84.pdf
Cyber-physical systems (CPS), which integrate computational and physical processes, present challenges in modeling, specification, and integration due to their heterogeneous nature and complex interactions. Contract-based design aims to address these challenges by using formal specifications to support hierarchical decomposition and system-level reasoning through contract manipulations. Combining this methodology with design automation, which leverages computational power to streamline design tasks, offers a promising approach to addressing the CPS design challenges.
This dissertation focuses on automating the contract-based design process to facilitate its application in cyber-physical system design. We identify the key design automation needs for contract-based design as specification, verification, simulation, and synthesis. Specification enables the expression of requirements and implementations as contracts while assisting in their manipulation. Verification detects potential errors in the decomposition process, ensuring a correct-by-construction design. Simulation provides insight into formal specifications by generating behaviors allowed by their semantics, helping designers confirm that contracts align with design intent and component characteristics. Synthesis automates the decomposition process and optimizes the design.
We address these needs by bridging key gaps in contract-based design automation. For specification, a new contract formalism, constraint-behavior contracts, is introduced to represent physical components using implicit equations, enabling precise expression of requirements. Verification techniques based on receptiveness and strong replaceability, a newly proposed contract relation, are developed to detect decomposition errors, including in feedback systems, ensuring correct-by-construction designs. We also propose a simulation framework that generates behaviors allowed by contract semantics and efficiently produces a small yet insightful set of examples to aid in validating contracts and localizing potential specification errors. A component selection algorithm combining black-box optimization with contract-based system reasoning is proposed to incorporate behaviors into the decomposition process and enable contract-based synthesis that addresses optimization objectives involving behaviors.
We integrate these contributions into ContractDA, the first tool for contract-based design to offer comprehensive design automation support, including specification, verification, simulation, and synthesis. ContractDA incorporates the proposed functionalities along with existing contract manipulations, offering an interface that enables designers and researchers to effectively apply contract-based design.
Advisors: Alberto L. Sangiovanni-Vincentelli
BibTeX citation:
@phdthesis{Yu:EECS-2025-84,
Author= {Yu, Sheng-Jung},
Title= {Automating Contract-based Design for Cyber-Physical Systems},
School= {EECS Department, University of California, Berkeley},
Year= {2025},
Month= {May},
Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-84.html},
Number= {UCB/EECS-2025-84},
Abstract= {Cyber-physical systems (CPS), which integrate computational and physical processes, present challenges in modeling, specification, and integration due to their heterogeneous nature and complex interactions. Contract-based design aims to address these challenges by using formal specifications to support hierarchical decomposition and system-level reasoning through contract manipulations. Combining this methodology with design automation, which leverages computational power to streamline design tasks, offers a promising approach to addressing the CPS design challenges.
This dissertation focuses on automating the contract-based design process to facilitate its application in cyber-physical system design. We identify the key design automation needs for contract-based design as specification, verification, simulation, and synthesis. Specification enables the expression of requirements and implementations as contracts while assisting in their manipulation. Verification detects potential errors in the decomposition process, ensuring a correct-by-construction design. Simulation provides insight into formal specifications by generating behaviors allowed by their semantics, helping designers confirm that contracts align with design intent and component characteristics. Synthesis automates the decomposition process and optimizes the design.
We address these needs by bridging key gaps in contract-based design automation. For specification, a new contract formalism, constraint-behavior contracts, is introduced to represent physical components using implicit equations, enabling precise expression of requirements. Verification techniques based on receptiveness and strong replaceability, a newly proposed contract relation, are developed to detect decomposition errors, including in feedback systems, ensuring correct-by-construction designs. We also propose a simulation framework that generates behaviors allowed by contract semantics and efficiently produces a small yet insightful set of examples to aid in validating contracts and localizing potential specification errors. A component selection algorithm combining black-box optimization with contract-based system reasoning is proposed to incorporate behaviors into the decomposition process and enable contract-based synthesis that addresses optimization objectives involving behaviors.
We integrate these contributions into ContractDA, the first tool for contract-based design to offer comprehensive design automation support, including specification, verification, simulation, and synthesis. ContractDA incorporates the proposed functionalities along with existing contract manipulations, offering an interface that enables designers and researchers to effectively apply contract-based design.},
}
EndNote citation:
%0 Thesis %A Yu, Sheng-Jung %T Automating Contract-based Design for Cyber-Physical Systems %I EECS Department, University of California, Berkeley %D 2025 %8 May 16 %@ UCB/EECS-2025-84 %U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-84.html %F Yu:EECS-2025-84