Compositional Hoare-style Reasoning about Hybrid CSP in the Duration Calculus

TL;DR

This paper introduces a novel Hoare-style reasoning framework for hybrid systems using Duration Calculus, unifying assertions and temporal conditions with a complete proof system for system verification.

Contribution

It proposes a new approach based on weakly monotonic time, Duration Calculus with infinite intervals, and a unified semantics for Hoare triples, enhancing reasoning about hybrid systems.

Findings

Developed a proof system complete relative to Duration Calculus validity.

Unified assertions and temporal conditions in Hoare-like triples.

Enhanced compositional reasoning for hybrid systems.

Abstract

Deductive methods for the verification of hybrid systems vary on the format of statements in correctness proofs. Building on the example of Hoare triple-based reasoning, we have investigated several such methods for systems described in Hybrid CSP, each based on a different assertion language, notation for time, and notation for proofs, and each having its pros and cons with respect to expressive power, compositionality and practical convenience. In this paper we propose a new approach based on weakly monotonic time as the semantics for interleaving, the Duration Calculus (DC) with infinite intervals and general fixpoints as the logic language, and a new meaning for Hoare-like triples which unifies assertions and temporal conditions. We include a proof system for reasoning about the properties of systems written in the new form of triples that is complete relative to validity in DC.