Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems

Fatma Jebali 1
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 several synchronous components that evolve concurrently, each with its own pace, and communicate altogether asynchronously. This thesis proposes a formal modelling and verification framework 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 synchronous components, asynchronous communication, and constraints involving both component paces and the data carried by component inputs. To analyse GRL specifications, we took advantage of the CADP software toolbox for the verification of asynchronous concurrent processes, using state space exploration techniques. For this purpose, we have defined a translation from GRL to the LNT specification language supported by CADP. The translation has been implemented by a tool named GRL2LNT, thus enabling state spaces to be automatically derived from GRL specifications. To enable the formal verification of GRL specifications, we have designed a property specification language, named muGRL, which is interpreted on GRL state spaces. The muGRL language is based on a set of patterns capturing properties of concurrent and GALS systems, which reduces the complexity of using full-fledged temporal logics. The semantics of muGRL are defined by a translation into the MCL temporal logic supported by CADP. Finally, we have illustrated how GRL, muGRL, and CADP can be applied to model and verify concrete GALS applications, including industrial case-studies.
Document type :
Theses
Computer Science [cs]. Inria - Research Centre Grenoble – Rhône-Alpes; Laboratoire d'Informatique de Grenoble; Université Grenoble Alpes, 2016. English
Liste complète des métadonnées


https://hal.inria.fr/tel-01511656
Contributor : Fatma Jebali <>
Submitted on : Friday, April 21, 2017 - 2:17:05 PM
Last modification on : Sunday, April 23, 2017 - 1:02:33 AM

Identifiers

  • HAL Id : tel-01511656, version 1

Collections

Citation

Fatma Jebali. Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems. Computer Science [cs]. Inria - Research Centre Grenoble – Rhône-Alpes; Laboratoire d'Informatique de Grenoble; Université Grenoble Alpes, 2016. English. <tel-01511656>

Share

Metrics

Record views

160

Document downloads

29