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 :
Theses
Computation and Language [cs.CL]. Université Grenoble Alpes, 2016. English. 〈NNT : 2016GREAM036〉
Liste complète des métadonnées

Cited literature [115 references]  Display  Hide  Download

https://tel.archives-ouvertes.fr/tel-01679311
Contributor : Abes Star <>
Submitted on : Tuesday, January 9, 2018 - 6:04:41 PM
Last modification on : Thursday, June 21, 2018 - 1:10:15 AM

File

JEBALI_2016_archivage.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-01679311, version 1

Collections

Citation

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〉

Share

Metrics

Record views

173

Files downloads

214