Abstract FR:

Nous proposons une methodologie de specification et de construction de systemes qui transforme la specification evenementielle d'un systeme en une specification pre-post, ce qui permet d'effectuer le processus de developpement a l'aide de techniques connues de derivation de programmes par raffinements et sans rompre le processus de raisonnement formel. Le role de la specification evenementielle est de decrire les interactions du systeme avec son environnement. Le resultat de la transformation est un module qui fournit les moyens de communication du systeme. Pour prendre en compte les aspects concurrents et distribues d'un systeme, nous proposons la notion de module partage. Nous utilisons des variables auxiliaires, non implantees, pour exprimer des proprietes abstraites et pour faire la preuve de correction des implantations effectuees. Pour repondre au besoin de reutilisation de modules existants, nous proposons une technique pour completer une specification a l'aide de variables auxiliaires afin de l'adapter a la solution de problemes particuliers, tout en preservant l'implantation fournie initialement.