Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems

Fatma Jebali 1
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Résumé : Un système GALS (Globalement Asynchrone, Localement Synchrone) est un ensemble de composants synchrones qui évoluent en même temps, chacun à son 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 Representation 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 modéliser et vérifier des applications GALS concrètes, comprenant des études de cas industrielles.
Type de document :
Thèse
Computer Science [cs]. Inria - Research Centre Grenoble – Rhône-Alpes; Laboratoire d'Informatique de Grenoble; Université Grenoble Alpes, 2016. English
Liste complète des métadonnées

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

https://hal.inria.fr/tel-01511656
Contributeur : Fatma Jebali <>
Soumis le : vendredi 21 avril 2017 - 14:17:05
Dernière modification le : jeudi 11 janvier 2018 - 06:23:43
Document(s) archivé(s) le : samedi 22 juillet 2017 - 12:56:54

Identifiants

  • HAL Id : tel-01511656, version 1

Collections

Citation

Fatma Jebali. Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems. Computer Science [cs]. Inria - Research Centre Grenoble – Rhône-Alpes; Laboratoire d'Informatique de Grenoble; Université Grenoble Alpes, 2016. English. 〈tel-01511656〉

Partager

Métriques

Consultations de la notice

212

Téléchargements de fichiers

90