Modular Analysis of Distributed Hybrid Systems using Post-Regions (Full Version)

TL;DR

This paper presents a modular verification approach for distributed hybrid systems using post-regions, extending rely-guarantee reasoning to hybrid settings and enabling efficient, compositional analysis.

Contribution

It generalizes rely-guarantee reasoning to hybrid systems and introduces a modular verification system based on post-regions for object-oriented distributed hybrid systems.

Findings

Verification system is implemented for HABS language.

Only one proof obligation per method is generated.

Post-region approximation can be achieved with lightweight analyses.

Abstract

We introduce a new approach to analyze distributed hybrid systems by a generalization of rely-guarantee reasoning. First, we give 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 also has to hold in the post-region of a method. The post-region describes all reachable states after method termination before another process is guaranteed to run. The system naturally generalizes rely-guarantee reasoning of discrete object-oriented languages to hybrid systems and carries over its modularity to hybrid systems: Only one dL-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.