Abstract FR:

L'objet de cette these est la specification des systemes informatiques. Nous avons, dans un premier temps, analyse la nature d'une specification afin d'extraire les caracteristiques d'une bonne methode de specification. Nous defendons, entre autres, les theses qu'une methode doit posseder une demarche permettant d'isoler les concepts importants comme les activites, les acteurs, les dependances temporelles mais aussi disposer d'un veritable langage, pourvu d'une semantique complete, permettant la simulation et la validation de la specification ainsi que la compilation ou la generation de code. Dans un deuxieme temps, nous presentons la methode armor, support de nos theses. La demarche d'analyse de armor se rapproche de celle de jackson system development (jsd) par la modelisation du monde reel en terme d'actions et de comportements (les activites et les acteurs) et par la specification du systeme en terme de processus communicants par envoi de messages et par inspections. Nous donnons une definition semantique rigoureuse qui rend armor compilable. Les originalites de armor resident dans la planarite de la specification qui n'est composee que de trois couches; dans l'organisation arborescente de la specification qui ne possede aucune semantique; dans une gestion totale du temps a l'instar des langages synchrones; et dans ses techniques de compilations qui s'inspirent soit des langages synchrones soit des synchroniseurs, soit des simulations distribuees dites optimistes. La derniere partie est consacree a la presentation de trois etudes de cas, montrant le large spectre d'application de armor. Nous construisons les specifications d'une simulation (le jeu de la vie), d'un systeme reactif (un regulateur de vitesse) et d'un systeme d'information (une gestion de bibliotheque)