Skip to Main content Skip to Navigation

Formal framework for modelling and verifying globally asynchronous locally synchronous systems

Abstract : A GALS (Globally Asynchronous, Locally Synchronous) system consists of several synchronouscomponents that evolve concurrently, each with its own pace, and communicatealtogether asynchronously. This thesis proposes a formal modelling and verificationframework dedicated to GALS systems, with a focus on the asynchronous behaviour.As a cornerstone of our framework, we have designed a formal language, named GRL(GALS Representation Language). GRL enables the behavioural specification of synchronouscomponents, asynchronous communication, and constraints involving bothcomponent paces and the data carried by component inputs. To analyse GRL specifications,we took advantage of the CADP software toolbox for the verification of asynchronousconcurrent processes, using state space exploration techniques. For this purpose,we defined a translation from GRL to the LNT specification language supportedby CADP. The translation was implemented by a tool named GRL2LNT, thus enablingstate spaces to be automatically derived from GRL specifications.To enable the formal verification of GRL specifications, we designed a property specificationlanguage, named muGRL, which is interpreted on GRL state spaces. The muGRLlanguage is based on a set of patterns capturing properties of concurrent and GALSsystems, which reduces the complexity of using full-fledged temporal logics. The semanticsof muGRL are defined by a translation into the MCL temporal logic supported byCADP. Finally, we illustrated how GRL, muGRL, and CADP can be applied to modeland verify concrete GALS applications, including industrial case-studies.
Document type :
Complete list of metadata

Cited literature [115 references]  Display  Hide  Download
Contributor : Abes Star :  Contact
Submitted on : Tuesday, January 9, 2018 - 6:04:41 PM
Last modification on : Thursday, November 19, 2020 - 1:00:01 PM


Version validated by the jury (STAR)


  • HAL Id : tel-01679311, version 1



Fatma Jebali. Formal framework for modelling and verifying globally asynchronous locally synchronous systems. Computation and Language [cs.CL]. Université Grenoble Alpes, 2016. English. ⟨NNT : 2016GREAM036⟩. ⟨tel-01679311⟩



Record views


Files downloads