Fatma Jebali - Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems

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 thesisproposes 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 RepresentationLanguage). 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 GRLspecifications, we took advantage of the CADP software toolbox for the verification of asynchronous oncurrent processes, using state space exploration techniques. For this purpose, we defined a translationfrom GRL to the LNT specification language supported by CADP. The translation was 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 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 supportedby CADP. Finally, we illustrated how GRL, muGRL, and CADP can be applied to model and verify concrete GALSapplications, including industrial case-studies.