Interpretation efficace d'expression de processus EB3

Malgre un nombre croissant de succes, les methodes formelles en genie logiciel restent encore limitees a un nombre de secteurs restreints de l'informatique. Principalement utilisees pour des systemes critiques, elles sont delaissees par le gros de l'industrie informatique qui voit en elles des methodes complexes a mettre en oeuvre, demandant une grande expertise et apportant une securite et une qualite trop cherement payees. C'est notamment le cas pour le domaine des systemes d'information, ou les methodes formelles ne sont pas considerees comme etant rentables. Pourtant, par leur importance croissante au sein de nos societes, les systemes d'information sont de plus en plus soumis a des imperatifs majeurs de fiabilite. De plus en plus complexes et important, ces systemes ont ete largement etudies et presentent, en fait, un profil parfait pour beneficier des apports d'une methode formelle. Il ne faut cependant pas faire fi des reticences des acteurs majeurs de cette industrie et leur fournir des outils adaptes a leur besoin. C'est dans cette optique qu'est ne le projet APIS [26] et la methode EB3 de Frappier et St-Denis [28] qui visent la construction d'une boite a outils permettant l'utilisation d'une methode de specification formelle, afin d'ameliorer la fiabilite des systemes d'information, mais aussi de diminuer les couts et l'effort de dveloppement et de maintenance de tels systemes. Pour cela, la methode recherchee se doit d'etre le plus intuitive, mais aussi d'automatiser la plus grande partie de la construction du systeme.;Pour cela, un interpreteur pour l'algebre de processus de la methode EB3 a ete concu afin de permettre la generation d'un systeme par interpretation de sa specification. En automatisant le processus de construction du systeme, EB3 PAI, l'interpreteur de la methode EB 3, assure la validite du systeme par rapport a sa specification, tout en supprimant les couts lies aux phases intermediaires. La presente these presente l'interpreteur EB3PAI ainsi que l'ensemble des optimisations qui ont ete apportees a l'interpreteur et a la methode EB 3. En premier lieu, le systeme de regles a ete modifie. Le nouveau systeme de regle utilise des environnements plutot que des substitutions, traite de maniere implicite les executions de transitions internes (les transitions lambda) et ajoute la gestion des specifications non deterministes. Ainsi, tout en beneficiant d'un algorithme simple pour une execution des transitions; de nombreuses ameliorations sont apportees, sans modification pour les createurs de specification. La deuxieme serie d'optimisation concernent plus specifiquement les systemes d'information. Il s'agit de gerer les associations entre entites qui sont souvent presentes en tres grand nombre dans ces systemes. Ameliorant donc la performance du systeme, la kappa-optimisation permet d'atteindre l'objectif de concurrencer les systemes ecrits a la main en termes d'espace memoire et de vitesse d'execution des transitions. Chaque optimisation est validee par une preuve assurant que l'interpretation est bien correcte vis-a-vis de la specification. Cet interpreteur est la pierre angulaire du projet APIS.