Formal framework for modelling and verifying globally asynchronous locally synchronous systems

Résumé : Un système GALS (Globalement Asynchrone, Localement Synchrone) est un ensemble de composants synchrones qui évoluent en même temps, chacun à propre rythme, et qui communiquent de manière asynchrone. Cette thèse propose un environnement formel de modélisation et de vérification dédié aux systèmes GALS, en se focalisant sur le comportement asynchrone.Notre environnement s’appuie sur un langage formel que nous avons conçu nommé GRL (GALS Représentation Language). GRL permet la spécification comportementale des composants synchrones, de la communication asynchrone, et des contraintes sur les rythmes des composants ainsi que sur les valeurs que prennent les entrées des composants. Pour analyser les spécifications GRL, nous utilisons CADP, une boîte à outils logicielle permettant la vérification de processus concurrents asynchrones par des techniques d'exploration d’espaces d’états. Dans ce but, nous avons défini une traduction de GRL vers LNT, un langage de spécification supporté par CADP. La traduction est implémentée dans un outil appelé GRL2LNT, permettant ainsi la génération automatique d’espaces d'états à partir de spécifications GRL.Pour permettre la vérification formelle des spécifications GRL, nous avons conçu un langage de propriétés nommé muGRL, qui est interprété sur les espaces d’états de GRL. Le langage muGRL est basé sur un ensemble de patrons qui capturent les propriétés des systèmes concurrents et des systèmes GALS, réduisant ainsi la complexité d'utiliser les logiques temporelles classiques. La sémantique de muGRL est définie par traduction vers MCL, le langage de logique temporelle fourni par CADP. Enfin, nous illustrons l’usage de GRL, muGRL et CADP pour la modélisation et la vérification d’applications GALS concrètes, comprenant des études de cas industrielles.
Type de document :
Thèse
Computation and Language [cs.CL]. Université Grenoble Alpes, 2016. English. 〈NNT : 2016GREAM036〉
Liste complète des métadonnées

Littérature citée [115 références]  Voir  Masquer  Télécharger

https://tel.archives-ouvertes.fr/tel-01679311
Contributeur : Abes Star <>
Soumis le : mardi 9 janvier 2018 - 18:04:41
Dernière modification le : jeudi 21 juin 2018 - 01:10:15

Fichier

JEBALI_2016_archivage.pdf
Version validée par le jury (STAR)

Identifiants

  • HAL Id : tel-01679311, version 1

Collections

Citation

Fatma Jebali. Formal framework for modelling and verifying globally asynchronous locally synchronous systems. Computation and Language [cs.CL]. Université Grenoble Alpes, 2016. English. 〈NNT : 2016GREAM036〉. 〈tel-01679311〉

Partager

Métriques

Consultations de la notice

174

Téléchargements de fichiers

215