Scholarlink

<p>We introduce a new approach for analyzing distributed hybrid systems based on a generalization of rely-guarantee reasoning. First, we present a system for deductive verification of class invariants and method contracts in object-oriented distributed hybrid systems. In a hybrid setting, the object invariant must not only be the post-condition of a method, but must also has to hold in its <i>post-region</i>. The post-region describes all reachable states <i>after</i> method termination and <i>before</i> another process is guaranteed to be scheduled, and is independent of the dynamics. The system naturally generalizes rely-guarantee reasoning from discrete object-oriented languages to hybrid systems and preserves its modularity to hybrid systems: only one <InlineEquation ID="IEq1"> <EquationSource Format="TEX">\(d\mathcal{L}\)</EquationSource> </InlineEquation>-proof obligation is generated per method. The post-region can be approximated using lightweight analyses and we give a general notion of soundness for such analyses. Post-region-based verification is implemented for the Hybrid Active Object language <b>HABS</b>.</p>

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

Modular analysis of distributed hybrid systems using post-regions

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年2月18日

查看全文
  • Eduard Kamburjan

摘要

We introduce a new approach for analyzing distributed hybrid systems based on a generalization of rely-guarantee reasoning. First, we present a system for deductive verification of class invariants and method contracts in object-oriented distributed hybrid systems. In a hybrid setting, the object invariant must not only be the post-condition of a method, but must also has to hold in its post-region. The post-region describes all reachable states after method termination and before another process is guaranteed to be scheduled, and is independent of the dynamics. The system naturally generalizes rely-guarantee reasoning from discrete object-oriented languages to hybrid systems and preserves its modularity to hybrid systems: only one \(d\mathcal{L}\) -proof obligation is generated per method. The post-region can be approximated using lightweight analyses and we give a general notion of soundness for such analyses. Post-region-based verification is implemented for the Hybrid Active Object language HABS.