Formal Modeling and Verification of GALS Systems Using GRL and CADP

Fatma Jebali 1, * Frédéric Lang 1, * Eric Léo 1 Radu Mateescu 1
* Auteur correspondant
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : The GALS (Globally Asynchronous, Locally Synchronous) paradigm is a prevalent approach to design distributed synchronous subsystems that communicate with each other asynchronously. The design of GALS systems is tedious and error-prone due to the complexity of architectures and high synchronous and asynchronous concurrency involved. This paper proposes a model-based approach to formally verify such systems. Specifications are written in GRL (GALS Representation Language), dedicated to model GALS systems with homogeneous syntax and formal semantics. We present a translation from GRL to LNT, a value-passing process algebra with imperative flavour. The translation is automated by means of the GRL2LNT tool, making possible the analysis of GRL specifications using the CADP toolbox. We illustrate our approach with an access management system for smart parking based on distributed software systems embedded in programmable logic controllers.
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger
Contributeur : Fatma Jebali <>
Soumis le : vendredi 14 novembre 2014 - 16:29:05
Dernière modification le : jeudi 11 octobre 2018 - 08:48:04
Document(s) archivé(s) le : vendredi 14 avril 2017 - 16:27:06


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01082950, version 1




Fatma Jebali, Frédéric Lang, Eric Léo, Radu Mateescu. Formal Modeling and Verification of GALS Systems Using GRL and CADP. 2014. 〈hal-01082950〉



Consultations de la notice


Téléchargements de fichiers