Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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 
* Corresponding author
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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Fatma Jebali Connect in order to contact the contributor
Submitted on : Friday, November 14, 2014 - 4:29:05 PM
Last modification on : Wednesday, July 6, 2022 - 4:24:11 AM
Long-term archiving on: : Friday, April 14, 2017 - 4:27:06 PM


Files produced by the author(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⟩



Record views


Files downloads