From post-conditions to post-region invariants: Deductive verification of hybrid objects

Abstract

We introduce a new system for object-oriented distributed hybrid systems to verify object invariants and method contracts. 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, because the state of the object evolves according to continuous dynamics. The post-region describes all reachable states after method termination before another process runs. This set can be approximated using lightweight analysis of the class structure. The system naturally generalizes rely-guarantee reasoning of discrete object-oriented languages to hybrid systems and carries over its compositionality to hybrid systems: only one dL-proof obligation is generated per method. By reasoning about the minimal size of the post-region, local Zeno behavior can also be analyzed. Our approach is implemented for the Hybrid Active Object language HABS.