GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems

Fatma Jebali, Frédéric Lang, and Radu Mateescu

Proceedings of the 16th International Conference on Formal Engineering Methods ICFEM'2014 (Luxembourg, Luxembourg), November 3-5, 2014


A GALS (Globally Asynchronous, Locally Synchronous) system consists of several synchronous subsystems that evolve concurrently and interact with each other asynchronously. Most formalisms and design tools support either the synchronous paradigm or the asynchronous paradigm but rarely combine both, which requires an intricate modeling of GALS systems. In this paper, we present a new language, called GRL (GALS Representation Language) designed to model GALS systems in an abstract and versatile manner for the purpose of formal verification. GRL has formal semantics combining the synchronous reactive model underlying dataflow languages and the asynchronous concurrent model underlying process algebras. We present the basic concepts and the main constructs of the language, together with an illustrative example.

16 pages


Slides of F. Jebali's lecture at ICFEM'2014: