Université de Rennes 1 On the mechanized verification of the meta-theory of contracts and its instantiation to differential dynamic logic Sur la vérification mécanisée de la méta-théorie des contrats et son instanciation à la logique dynamique différentielle Méthodes formellesconception par contratssystèmes cyber-physiques Formal methodscontract-based designcyber physical systems Méthodes formelles (informatique) Objets coopérants (informatique) 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. 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. Electronic Thesis or DissertationText en application/pdf1 : 1438 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/a4d6c985-3aef-4a84-8953-fcd5c498569f Kastenbaum Stéphane 1996-02-28 FR 271703660 stephane.kastenbaum@gmail.com 2023URENS013 http://www.theses.fr/2023URENS013 2023-05-05 Informatique Université de Rennesthesis.degree.grantor_1 26693823X Doctorat non ouiTalpinJean-Pierreintervenant_1094211515BoyerBenoîtintervenant_2151807663HuguesJérômeintervenant_3105679569LaleauRégineintervenant_4150895194BoyerBenoîtintervenant_6151807663HuguesJérômeintervenant_3105679569MerryDominiqueintervenant_527170411X MATISSEecoleDoctorale_1 267602553 INRIA-RENNES partenaireRecherche_1 133175863 ddc:004 TalpinJean-PierreBoyerBenoîtHuguesJérômeLaleauRégineMerryDominiqueBoyerBenoîtUniversité de RennesMATISSE INRIA-RENNES ASCII PDF 1472189