Une methode a multi-formalismes pour la specification et la validation de systemes distribues
Institution:
Paris 6Disciplines:
Directors:
Abstract EN:
Pas de résumé disponible.
Abstract FR:
La complexite de mise en uvre des systemes distribues est liee aux problemes d'organisation des differentes actions a mener pour la specification, conception, verification, et developpement de ces systemes, mais aussi, a la difficulte de maitriser dynamiquement, les interactions de multitudes entites uvrant en paralleles, communiquant, cooperant et partageant des ressources communes. Le but de cette these est d'etudier les problemes de complexite de specification de systemes distribues et de proposer une approche methodologique pour les resoudre. L'approche formelle pour le developpement de systemes semble prometteuse, neanmoins, elle souffre d'une certaine reticence de la part des industriels a cause du niveau technique necessaire a leur utilisation et au peu d'outils disponibles sur le marche. La solution proposee est basee sur des techniques semi-formelles pour la specification de haut niveau et formelles pour la specification de bas niveau permettant la validation du systeme specifie. Elle permet ainsi d'aider et de guider le concepteur tout le long du processus de developpement. Le processus de developpement est base sur le concept multi-formalisme et sur les processus d'enrichissement et de transformation. Le concept multi-formalisme permet d'utilisation, a chaque phase du processus de developpement, un ou plusieurs formalismes permettant de repondre aux objectifs de cette phase (entites/relations, reseaux en canaux-agences, reseaux de petri colores et type de donnees algebriques). Le role des processus d'enrichissement et de transformation fournir un moyen une progression coherent de la description du systeme, de la phase d'analyse des besoins jusqu'a la phase de generation de code. Un environnement de support de la methodologie a ete developpe facilitant ainsi la specification et la validation d'applications. Enfin, cette approche a ete experimentee et validee par la specification d'une application: achat electronique