Formal Modelling and Verification of GALS Systems Using GRL and CADP - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Formal Aspects of Computing Année : 2016

Formal Modelling and Verification of GALS Systems Using GRL and CADP

Résumé

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.
Fichier principal
Vignette du fichier
fac2egui-crc.pdf (598.85 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01290449 , version 1 (18-03-2016)

Identifiants

Citer

Fatma Jebali, Frédéric Lang, Radu Mateescu. Formal Modelling and Verification of GALS Systems Using GRL and CADP. Formal Aspects of Computing, 2016, 28 (5), pp.767-804. ⟨10.1007/s00165-016-0373-3⟩. ⟨hal-01290449⟩
434 Consultations
293 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More