Scholarlink

Modeling Cyber-Physical Systems (CPS) with timing constraints is challenging due to the complexity of their component behaviors. We propose “Timed SysReo”, a novel modeling language that extends SysML with Timed Reo to capture CPS architecture and timed interactions. Timed SysReo uses Timed Reo Internal Block Diagrams (Timed Reo IBD) and Timed SysReo Sequence Diagrams (TSRSD) to detail component interactions and message flows. Since direct formal verification of requirements in TSRSD is impractical, we automate the transformation of TSRSD into Timed Constraint Automata (TCA) using ATL rules. Requirements are expressed in Timed Scheduled-Data-Stream Logic (TSDSL), enhancing precision and rigor in CPS verification. We illustrate the efficacy of our approach through a case study involving a Smart Medical Bed (SMB).

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

Integrating SysML and Timed Reo to Model and Verify Cyber-Physical Systems Interactions with Timing Constraints

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Perla Tannoury,
  • Ahmed Hammad

摘要

Modeling Cyber-Physical Systems (CPS) with timing constraints is challenging due to the complexity of their component behaviors. We propose “Timed SysReo”, a novel modeling language that extends SysML with Timed Reo to capture CPS architecture and timed interactions. Timed SysReo uses Timed Reo Internal Block Diagrams (Timed Reo IBD) and Timed SysReo Sequence Diagrams (TSRSD) to detail component interactions and message flows. Since direct formal verification of requirements in TSRSD is impractical, we automate the transformation of TSRSD into Timed Constraint Automata (TCA) using ATL rules. Requirements are expressed in Timed Scheduled-Data-Stream Logic (TSDSL), enhancing precision and rigor in CPS verification. We illustrate the efficacy of our approach through a case study involving a Smart Medical Bed (SMB).