Abstract FR:

Cette these participe a l'effort mene actuellement autour des techniques de description formelles (fdt) normalisees a l'iso: lotos (language of temporal ordering specification) et estelle (extended finite state machine language). Plus particulierement, elle vise a l'amelioration de l'usage de lotos sur les plans de la specification et de l'implementation. Dans une premiere partie on a presente une interface graphique pour lotos rendant ce langage accessible aux specificateurs de systemes. La deuxieme partie decrit un modele/langage de pre-implementation primol (pre-implementation of lotos), ayant le meme domaine semantique (systemes de transitions etiquetes) que lotos, primol est la premiere etape formelle de lotos vers l'implementation qui permet de verifier, transformer et deriver des implantations a partir de specifications lotos. L'outil pil (pre-implementation of lotos) est propose comme un outil de pre-implementation de lotos base sur le modele/langage primol. Pil permet de traduire des specifications lotos en pre-implementations primol elles-memes transformables en primol