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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Review: Contract-Based Design Methodologies for Cyber-Physical Systems

  • Nadra Tabassam,
  • Martin Fränzle,
  • Muhammad Waleed Ansari,
  • Ghazala Shaheen

摘要

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.