Exploitation des structures régulières et des spécifications locales pour le développement correct de systèmes réactifs de grande taille
Lionel Morel · HAL (Le Centre pour la Communication Scientifique Directe) · 2005
The work presented in this thesis takes place in the domain of programming and validation of synchronous reactive systems. It aims at taking certain forms of structure of programs into account during the development and validation process. We first study the use of regular operators called "iterators" which allow to express in a quit natural way regular programs that manipulate arrays. On a validation point of view, we show how to take these regular structures into account in order to facilitate the proof of properties. In parallel to those iterators, we investigate a form of specification called assume-guarantee contracts where a couple of properties are used to specify some hypothesis of a component upon its environment and some property that the component satisfies whenever the hypothesis on the environment is satisfied. We show the interest of such contracts in terms of specification and verifi cation for the particular case of the synchronous systems. We finally propose a a series of program transformation algorithms, both for the iteration and the contract aspects that can be used as a pre-processor of proof objectives for validation tools. Our proposals, in particular on the language aspect of the iterators, met needs of several industrial applications, notably around the language Lustre, to which we apply our result. These propositions will soon be added to the industrial version of the language.