Formal Modelling and Verification of GALS Systems Using GRL and CADP

Fatma Jebali 1 Frédéric Lang 1 Radu Mateescu 1
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : A GALS (Globally Asynchronous, Locally Synchronous) system consists of several synchronous components that evolve concurrently and interact with each other asynchronously. The design of GALS systems is tedious and error-prone due to the high degree of synchronous and asynchronous concurrency present in complex architectures. In this paper, we present GRL (GALS Representation Language), a formal language designed to model GALS systems, for the purpose of formal verification of the asynchronous aspects. GRL combines the synchronous reactive model underlying dataflow languages and the asynchronous concurrent model underlying process algebras. We propose a translation from GRL to LNT, a value-passing concurrent language with classical process algebra flavour. This makes possible the analysis of GRL specifications using all the state-of-the-art simulation and verification functionalities provided by the CADP toolbox.
Type de document :
Article dans une revue
Formal Aspects of Computing, Springer Verlag, 2016, 28 (5), pp.767-804. 〈10.1007/s00165-016-0373-3〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01290449
Contributeur : Frederic Lang <>
Soumis le : vendredi 18 mars 2016 - 10:51:29
Dernière modification le : jeudi 11 janvier 2018 - 06:23:43
Document(s) archivé(s) le : lundi 20 juin 2016 - 01:33:09

Fichier

fac2egui-crc.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Fatma Jebali, Frédéric Lang, Radu Mateescu. Formal Modelling and Verification of GALS Systems Using GRL and CADP. Formal Aspects of Computing, Springer Verlag, 2016, 28 (5), pp.767-804. 〈10.1007/s00165-016-0373-3〉. 〈hal-01290449〉

Partager

Métriques

Consultations de la notice

332

Téléchargements de fichiers

151