Vérification et synthèse de systèmes réactifs
David Lesens · HAL (Le Centre pour la Communication Scientifique Directe) · 1997
This thesis concern is the verification of large reactive systems. Reactive systems are computer systems which react continuously to their physical environment, at a speed fixed by this environment. They are especially used for the control of critical systems: transport, nuclear, command of industrial processes, communication... For these uses, they must satisfy some critical working constraints. The verification of large reactive systems can be performed using modular decomposition of the program. Synthesis algorithms are proposed, allowing the construction of the most general subprograms, such that the complete system satisfies a given property. Modular verification has been extended to the case of parameterized networks of processes. The use of synchronous observers allows to specify properties on any number of processes. The proposed technique consists then in expressing an invariant of this network as a least or a greatest fixpoint, and in using extrapolation techniques to compute a regular approximation of these fixpoints. The cases of linear networks (or ring networks) and of tree networks have been particularly studied. All these techniques and algorithms have been implemented in a tool: a Boolean Automaton Network Grammar checker.