On the mechanized verification of the meta-theory of contracts and its instantiation to differential dynamic logic
Stéphane Kastenbaum · HAL (Le Centre pour la Communication Scientifique Directe) · 2023
The increasing complexity and heterogeneity of safe-critical systems present a challenge in designing and ensuring their safety. Formal methods are employed to validate system models, but the difficulty lies in verifying the safety at the global level, starting from validated component specifications. Contract theory addresses this problem by using assume/guarantee contracts as component specifications. The theory is equipped with operators for combining contracts and incrementally building a verified specification from the low-level functional requirements up to system-level requirements. Concretely, a contracts abstract component interfaces as pairs of assumptions-guarantees, specifying component-environment relations. This thesis introduces the mechanized formalization of an assume/guarantee contracts algebra in the calculus of construction of the proof assistant Coq. In the meantime, the formalization has been proven correct against the Benveniste et al.’s meta-theory formalized in Coq for all the necessary operators: composition, conjunction, abstraction, refinement, as well as the variable introduction and elimination. The practical use case of the contract model is demonstrated with differential dynamic logic and two instances of the contracts model. The theory is exercised on a case study to illustrate its power in modeling components and contractual abstractions.