Skip to Main content Skip to Navigation

GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems (Syntax and Formal Semantics)

Fatma Jebali 1, * Frédéric Lang 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 : A GALS (Globally Asynchronous, Locally Synchronous) system consists of a set of synchronous subsystems executing concurrently and interacting using an asynchronous communication scheme. Such systems involve a high degree of synchronous and asynchronous concurrency which makes challenging the design and debugging of applications. The use of formal methods in the design process helps designers to master that complexity and to build strong confidence in the correctness of these, usually safety-critical, systems. This report presents GRL (GALS Representation Language), a new formal language to specify GALS system for the purpose of formal verification, to provide design process with efficiency and correctness. GRL has a user-friendly syntax close to classical programming languages and an operational semantics combining the synchronous reactive paradigm inspired by classical data-flow languages and the asynchronous paradigm inspired by value-passing process algebras.
Complete list of metadata
Contributor : Fatma Jebali Connect in order to contact the contributor
Submitted on : Tuesday, September 16, 2014 - 1:42:41 PM
Last modification on : Wednesday, February 2, 2022 - 3:57:01 PM
Long-term archiving on: : Wednesday, December 17, 2014 - 10:56:46 AM


Files produced by the author(s)


  • HAL Id : hal-00983711, version 3


Fatma Jebali, Frédéric Lang, Radu Mateescu. GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems (Syntax and Formal Semantics). [Research Report] RR-8527, INRIA. 2014. ⟨hal-00983711v3⟩



Record views


Files downloads