On the mechanized verification of the meta-theory of contracts and its instantiation to differential dynamic logic

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.

 

L'augmentation de la complexité et de l'hétérogénéité des systèmes critiques pose un défi dans leur conception et leur assurance de sécurité. Les méthodes formelles sont utilisées pour valider les modèles de système, mais la difficulté réside dans la vérification de la sécurité du système global à partir des spécifications de composants validées. La théorie des contrats résout ce problème en utilisant les contrats d'assomption/garantie comme spécifications de composants. Les contrats sont validés en vérifiant que leurs hypothèses et garanties sur-approximent les pré- et post-conditions résultant des évaluations valides du modèle de composant. Les contrats individuels peuvent être combinés en faisant correspondre les hypothèses et garanties de chaque composant. Le manuscrit définit une formalisation algébrique des contrats d'assomption/garantie implémenté dans le calcul de construction de l'assistant de preuve Coq. Cette formalisation est prouvée pour valider une méta-théorie des contrats de Benveniste et al. pour tous les opérateurs tels que la composition, la conjonction, l'abstraction, le raffinement ainsi que l'introduction et l'élimination de variables. Le cas d'utilisation pratique du modèle de contrat est illustré avec la logique différentielle dynamique et deux instances du modèle de contrats. La théorie est appliquée à une étude de cas pour illustrer sa puissance dans la modélisation de composants pour valider un système cyber-physique.