Formalizing Time and Causality in Polychronous Polytimed Models

Résumé : L'intégration de composants dans un système peut s'avérer difficile lorsque ces composants ont été conçus selon différents paradigmes ou s'ils se basent sur différents cadres de temps devant être synchronisés. Cette synchronisation peut être dirigée par les évènements (un évènement est provoqué par un autre), ou dirigée par le temps (un évènement se produit parce qu'il en est l'heure). En considérant que chaque composant admet son propre cadre de temps et qu'ils peuvent ne pas être reliés, il est possible qu'une unique ligne de temps globale n'existe pas.Nous nous intéressons à la spécification de schémas de synchronisation pour de tels systèmes polychrones et polytemporisés. Notre étude nous a mené à la conception de modèles sémantiques pour un langage temporisé à évènements discrets, appelé TESL et développé par Boulanger et al. Ce langage a été utilisé pour coordonner la simulation de modèles composites et pour tester l'intégration de systèmes.Dans cette thèse, nous présentons une sémantique dénotationnelle fournissant une compréhension précise et logiquement cohérente du langage. Puis nous proposons une sémantique opérationnelle afin de dériver des traces d'exé-cutions satisfaisant une spécification TESL. Celui-ci a été utilisé pour les problématiques de test des systèmes, à travers l'implantation d'un solveur nommé Heron. Pour résoudre la question de cohérence et de correction de ces règles sémantiques, nous avons également développé une sémantique intermédiaire coinductive reliant les deux sémantiques dénotationnelles et opérationnelles. Nous établissons des propriétés sur la relation entre les deux sémantiques: correction, complétude, progrès ainsi que terminaison locale. Enfin, notre formalisation ainsi que les preuves associées ont été entièrement mécanisées dans l'assistant de preuve Isabelle/HOL.
Type de document :
Thèse
Modeling and Simulation. Université Paris-Saclay, 2018. English. 〈NNT : 2018SACLS282〉
Liste complète des métadonnées

https://tel.archives-ouvertes.fr/tel-01892649
Contributeur : Abes Star <>
Soumis le : mercredi 10 octobre 2018 - 17:30:06
Dernière modification le : jeudi 25 octobre 2018 - 12:59:05

Fichier

76327_NGUYEN_VAN_2018_archivag...
Version validée par le jury (STAR)

Identifiants

  • HAL Id : tel-01892649, version 1

Citation

Hai Nguyen Van. Formalizing Time and Causality in Polychronous Polytimed Models. Modeling and Simulation. Université Paris-Saclay, 2018. English. 〈NNT : 2018SACLS282〉. 〈tel-01892649〉

Partager

Métriques

Consultations de la notice

165

Téléchargements de fichiers

95