Modular analysis of distributed hybrid systems using post-regions

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.