Abstract FR:

Les methodes les plus utilisees en conception des systemes d'information sont basees principalement sur l'utilisation de diverses notations semi-formelles (diagrammes d'objets, diagrammes etats/transitions, ) qui presentent des avantages indeniables : puissance d'expression, vue graphique et synthetique du systeme d'information, faculte de communication avec les utilisateurs. Cependant il leur manque les qualites de concision, de precision et la possibilite de preuves des methodes formelles (basees en particulier sur la logique et la theorie des ensembles). Ce travail s'inscrit dans le cadre de l'integration des methodes semi-formelles et formelles. L'objectif de ce travail est de combiner leurs avantages respectifs en fournissant des regles de derivation de specifications formelles (en particulier en b) a partir de specifications semi-formelles (en particulier par objets). Tout d'abord, nous selectionnons les concepts les plus repandus des methodes semi-formelles et examinons precisement leur semantique. Cet examen nous conduit souvent a effectuer un choix entre plusieurs interpretations possibles des notations semi-formelles et meme a les completer lorsqu'elles s'averent insuffisantes pour decrire des situations reelles. Puis nous donnons des regles de traduction des concepts des modeles semi-formels en b. Notre objectif est de proposer des regles de derivation menant a une specification formelle a la fois comprehensible, fidele a la specification semi-formelle de depart, et modulaire afin de permettre des preuves incrementales et la reutilisation des composants. Afin de valider la methode de derivation, sont presentees trois etudes de cas developpees sous l'atelier b en appliquant nos regles.