Réduction paramétrée de spécifications formées d'automates communicants : algorithmes polynomiaux pour la réduction de modèles
Sebastien Labbé · HAL (Le Centre pour la Communication Scientifique Directe) · 2007
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.