Un système GALS (Globalement Asynchrone, Localement Synchrone) est un ensemble de composants synchrones qui évoluent en même temps, chacun à propre rythme, et qui communiquent de manière asynchrone. Cette thèse propose un environnement formel de modélisation et de vérification dédié aux systèmes GALS, en se focalisant sur le comportement asynchrone.Notre environnement s’appuie sur un langage formel que nous avons conçu nommé GRL (GALS Représentation Language). GRL permet la spécification comportementale des composants synchrones, de la communication asynchrone, et des contraintes sur les rythmes des composants ainsi que sur les valeurs que prennent les entrées des composants. Pour analyser les spécifications GRL, nous utilisons CADP, une boîte à outils logicielle permettant la vérification de processus concurrents asynchrones par des techniques d'exploration d’espaces d’états. Dans ce but, nous avons défini une traduction de GRL vers LNT, un langage de spécification supporté par CADP. La traduction est implémentée dans un outil appelé GRL2LNT, permettant ainsi la génération automatique d’espaces d'états à partir de spécifications GRL.Pour permettre la vérification formelle des spécifications GRL, nous avons conçu un langage de propriétés nommé muGRL, qui est interprété sur les espaces d’états de GRL. Le langage muGRL est basé sur un ensemble de patrons qui capturent les propriétés des systèmes concurrents et des systèmes GALS, réduisant ainsi la complexité d'utiliser les logiques temporelles classiques. La sémantique de muGRL est définie par traduction vers MCL, le langage de logique temporelle fourni par CADP. Enfin, nous illustrons l’usage de GRL, muGRL et CADP pour la modélisation et la vérification d’applications GALS concrètes, comprenant des études de cas industrielles. / 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.
| Identifer | oai:union.ndltd.org:theses.fr/2016GREAM036 |
| Date | 12 September 2016 |
| Creators | Jebali, Fatma |
| Contributors | Grenoble Alpes, Mateescu, Radu, Lang, Frédéric |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.0021 seconds