Review: Contract-Based Design Methodologies for Cyber-Physical Systems
摘要
Cyber-physical systems (CPSs) pose unique challenges due to their inherent heterogeneity, encompassing diverse physical elements, IT monitoring, and communication networks. Essential properties such as performance, safety, reliability, conformity with regulations, composability, modularity, and traceability across design levels are vital for successful CPS deployment. Contract-based design (CBD), rooted in Assume-Guarantee (A/G) reasoning, addresses these challenges. It facilitates refinement, composability, hierarchical verification, and modular verification of global properties by decomposing them into component-local contracts. CBD’s efficacy lies in proving the satisfaction of global properties through verification steps, demonstrating that local contracts collectively imply global ones, and validating local contractual properties by components. CBD finds extensive application across industries, adopting informal, semi-formal, and formal design paradigms across various development processes. Despite its widespread adoption, existing CBD frameworks incompletely cover conceivable system properties. To pinpoint areas for improvement and drive relevant research, this paper reviews different CBD techniques from functional system design, safety assessment, and system verification perspectives for CPSs and related complex technical systems. This review highlights open issues in CBD, signaling the need for further refinement and enhancement.