Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Thèses et habilitations
Production scientifique
Doctorat de

Doctorat
Equipe : Vérification d'Algorithmes, Langages et Systèmes

Formalizing Time and Causality in Polychronous Polytimed Models

Début le 01/10/2014
Direction : WOLFF, Burkhart

Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Sud

Lieu de déroulement : LRI - VALS

Soutenue le 27/09/2018 devant le jury composé de :
Directeurs de thèse :
- Frédéric Boulanger, CentraleSupélec
- Burkhart Wolff, Université Paris-Sud

Rapporteurs :
- Frédéric Mallet, Université Nice Sophia Antipolis
- Stephan Merz, Inria Nancy

Examinateurs :
- Catherine Dubois, ENSIIE
- Timothy Bourke, Inria Paris
- Marc Pantel, Université de Toulouse
- Mihaela Sighireanu, Université Paris Diderot

Activités de recherche :

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.