Recherche avancée
Toutes les thèses
Thèses de doctorat
Thèses d'exercice (médecine, santé, pharmacie)
Thèses de doctorat > Par auteur
Nouveautés
Par thématique
Par laboratoire
Par date
Par auteur
Thèses de doctorat -> Auteurs
Auteurs
>
K
>
Kastenbaum Stéphane
Niveau supérieur
1
ressource a été trouvée.
|<
<< Page précédente
1
Page suivante >>
>|
5
10
15
20
25
30
35
40
documents par page
Tri :
Date
Titre
Auteur
On the mechanized verification of the meta-theory of contracts and its instantiation to differential dynamic logic
Informatique / 05-05-2023
Kastenbaum Stéphane
Voir le résumé
Voir le résumé
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.
|<
<< Page précédente
1
Page suivante >>
>|
5
10
15
20
25
30
35
40
documents par page
© 2016
|
MENTIONS LEGALES
|
PLUS D'INFORMATION