Scholarlink

<p>Hybrid automata networks (HANs) provide a powerful formalism to represent interactions within distributed hybrid systems, where each subsystem exhibits both continuous and discrete dynamics. Although the properties of HANs can be verified by model checking exhaustively, the effectiveness of the verification process is challenged by the state explosion problem inherent in large-scale HANs. This research proposes <span>shan</span>, a novel verification framework specifically designed for HANs. <span>shan</span> employs task scenarios in the form of sequence diagrams to facilitate the verification of HANs. It systematically navigates the state spaces that developers consider important. The task scenarios and the HAN under verification are encoded as SMT formulas to simulate the execution of the HAN to accelerate the verification. The framework accelerates the verification process further using parallelization and minimal unsatisfiable core techniques for efficient instruction pruning. Moreover, we introduce metrics designed to evaluate the extent of HAN verification coverage, providing developers with a comprehensive tool for assessing the completeness of HAN verification.</p>

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

Verifying hybrid automata networks guided by task scenarios

  • 期刊论文

  • 发表日期：

    2026年2月25日

查看全文
  • Longlong Lu,
  • Yufei Shi,
  • Minxue Pan,
  • Xuandong Li

摘要

Hybrid automata networks (HANs) provide a powerful formalism to represent interactions within distributed hybrid systems, where each subsystem exhibits both continuous and discrete dynamics. Although the properties of HANs can be verified by model checking exhaustively, the effectiveness of the verification process is challenged by the state explosion problem inherent in large-scale HANs. This research proposes shan, a novel verification framework specifically designed for HANs. shan employs task scenarios in the form of sequence diagrams to facilitate the verification of HANs. It systematically navigates the state spaces that developers consider important. The task scenarios and the HAN under verification are encoded as SMT formulas to simulate the execution of the HAN to accelerate the verification. The framework accelerates the verification process further using parallelization and minimal unsatisfiable core techniques for efficient instruction pruning. Moreover, we introduce metrics designed to evaluate the extent of HAN verification coverage, providing developers with a comprehensive tool for assessing the completeness of HAN verification.