Réduction paramétrée de spécifications formées d'automates communicants : algorithmes polynomiaux pour la réduction de modèles
Institution:
Paris 6Disciplines:
Directors:
Abstract EN:
This PhD thesis is concerned with formal methods for languages of communicating automata specifications. In the industry, this kind of languages is mainly used in fields where the reliability requirements are high (e. G. Aeronautical, transportation industries), as a mean of improving the precision of specifications, and exploiting simulation, testing and verification tools, for the purpose of specification validation. Still, on large scale industrial specifications, formal methods suffer from the combinatorial explosion phenomenon; this is notably due to the manipulation of wide numerical domains, and the specifications inner parallelism. In our contribution, we suggest to bypass this phenomenon, in applying slicing techniques before the targeted complex analysis. This analysis can thus be performed a posteriori on a reduced (or sliced) specification, which is potentially less exposed to combinatorial explosion. Our slicing method is based on dependence relations, defined on the specification under analysis, and is mainly founded on the literature on compiler construction and program slicing. In this thesis, we state a theoretical framework for static analyses of communicating automata specifications, in which we formally define the aforementioned dependence relations, together with the concept of a slice of a specification with respect to a slicing criterion. Then, we describe and prove the efficient algorithms that we designed for calculating dependence relations and specification slices. Finally, we describe our implementation of these algorithms in the Carver tool, for slicing communicating automata specifications.
Abstract FR:
Cette thèse s'inscrit dans le cadre des méthodes formelles pour les spécifications formées d'automates communicants. Les applications industrielles de ces méthodes sont limitées par l'explosion combinatoire. L’idée que nous proposons consiste à contourner ce phénomène en appliquant des techniques de réduction paramétrée, en amont d'une analyse complexe. Celle-ci peut ainsi être effectuée a posteriori sur une spécification réduite, donc moins sujette à l'explosion combinatoire. Notre méthode de réduction paramétrée est basée sur des relations de dépendances dans la spécification analysée. Nous établissons un cadre théorique pour les analyses statiques de spécifications, dans lequel nous définissons formellement les relations de dépendances mentionnées ci-dessus, ainsi que le concept de tranche de spécification par rapport à un critère de réduction. Ensuite, nous décrivons et démontrons les algorithmes que nous avons mis au point et implanté, pour calculer les dépendances et les tranches.