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

https://hal.inria.fr/hal-01082950
Contributor : Fatma Jebali <>
Submitted on : Friday, November 14, 2014 - 4:29:05 PM
Last modification on : Tuesday, February 9, 2021 - 3:10:03 PM
Long-term archiving on: : Friday, April 14, 2017 - 4:27:06 PM

File

etaps-2015.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01082950, version 1

Collections

Relations

Citation

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⟩

Share

Metrics

Record views

433

Files downloads

233