L4.1 : Validation fonctionnelle de l'architecture

La complexite inherente aux protocoles de gestion de groupe securises et hierarchises etudies dans le cadre du projet SAFECAST justifie le recours a des techniques de modelisation et verification formelle. Il est maintenant admis (voir le « point dur » correspondant dans le L 4.2) qu'une campagne de verification menee avec un seul outil ne permet pas traiter a la fois les aspects « securite » et « contraintes temporelles » des exigences exprimees dans le L4.3. C'est pourquoi il a ete decide d'utiliser deux outils de verification formelle, a savoir AVISPA [AVISPA] et TURTLE [TURTLE] [TOOL]. Ces deux outils sont complementaires dans la mesure ou ils sont specialises sur la securite pour ce qui concerne AVISPA et sur les contraintes temporelles pour ce qui est de TURTLE. Le fait de travailler avec deux outils ayant chacun leur langage de modelisation propre pose le probleme de la coherence des deux modeles developpes. La premiere reponse apportee dans ce rapport est la description (en UML) du service offert par le systeme SAFECAST (tant du point de vue de la securite que de la gestion intra et inter groupes). La deuxieme reponse reside dans l'enonce d'hypotheses de modelisation communes aux developpeurs des modeles TURTLE et AVISPA. Au-dela des modeles developpes pour chacun de ces deux outils et presentes in extenso en annexe, le corps de ce rapport met l'accent sur les exigences non satisfaites et propose des correctifs. A titre de synthese, un tableau des exigences precise pour chacune d'elle si elle a pu etre verifiee et dans l'affirmative quel(s) outil(s) a (ont) ete utilise(s).