Évaluation des bornes des performances temporelles des Architectures d'Automatisation en Réseau par preuves itératives de propriétés logiques
Silvain Ruel · HAL (Le Centre pour la Communication Scientifique Directe) · 2009
This thesis proposes an approach to obtain the bounds of temporal performances of a Networked Automation Architecture by iterative proofs of reachability properties on a formal model of the architecture. These reachability properties are defined by means of a parametric timed observer automaton, whose guards of transitions are based on a time parameter. At each iteration, the results of proofs are used to calculate the value of this parameter for the next iteration; a dichotomy algorithm ensures the convergence of iterations. The implementation of this approach on nontrivial architectures has required the development of an abstraction method which comprises two steps: simplification of the structure and modification of formal models of the components contained in the simplified structure in order to take into account the phenomena of concurrency between requests emitted by different components. These formal and methodological contributions have been validated experimentally by the treatment of several case studies of increasing complexity and size, based on Modbus TCP / IP.