TUTORIEL n° 1

Introduction à la modélisation de systèmes réactifs avec UML
et les langages synchrones

Emmanuel LEDINOT
Dassault Aviation (Saint-Cloud)
Responsable du service Etudes Scientifiques Amont de la Direction de la
Prospective

Profil : Ingénieur Recherche & Développement chez Dassault Aviation.

Travaille depuis une quinzaine d'années sur les méthodes de spécification formelle de logiciel (langages synchrones, types abstraits algébriques, VDM, UML et langages objets, ML et Calcul des Constructions Inductives), ainsi que sur les techniques de preuve de programme appliquées à la sûreté des logiciels critiques embarqués.

TUTORIEL n° 2

RoZ, un outil intégrant UML et Z pour l'ingénierie des exigences

Y. Ledru et S. Dupuy
LSR,CLIPS/IMAG
Grenoble
Yves.Ledru@imag.frEmmanuel LEDINOT

Les notations graphiques semi-formelles, comme UML, constituent aujourd'hui l'un des outils majeurs de description des exigences, notamment pour les systèmes d'information. Dans ce cours, nous montrons comment ces notations peuvent être intégrées avec des méthodes formelles comme Z. Le but de cette intégration est de combiner les points forts des deux approches:

• les langages graphiques offrent une notation intuitive qui facilite la communication entre l'analyste et son client;
• ils correspondent à une pratique industrielle courante;
• les méthodes formelles augmentent la précision des spécifications;
• cette précision peut être exploitée par des outils de simulation, de test ou de vérification qui contribuent à la validation des spécifications.

Ce cours se base sur l'expérience que nous avons acquise en développant et en utilisant l'outil RoZ qui intègre des annotations en Z au diagramme de classes d'UML.

Notre approche se fonde sur des règles de traduction qui ont été implantées dans l'outil RoZ. L'étude de ces règles permet de comprendre les limites de la notation graphique. Elle nous a permis d'identifier une hiérarchie d'annotations qui complètent ces diagrammes. Cette hiérarchie peut être exploitée tant pour des annotations formelles que pour des annotations en
langue naturelle.

Cette approche est d'abord une aide à la production de spécifications : les diagrammes expriment la structure des spécifications et l'expression formelle est restreinte aux annotations qui expriment le typage, des contraintes ou décrivent des opérations. La traduction systématique de la structure peut être exploitée pour augmenter l'automatisation d'outils d'analyse.

L'outil RoZ, qui réalise cette traduction, est intégré dans un environnement UML commercial. L'analyste utilise donc son environnement habituel pour développer ses diagrammes et, le cas échéant, les compléter avec des annotations exprimées en Z. La spécification annotée est ensuite traduite en une seule spécification Z où certaines propriétés de cohérence peuvent être démontrées (existence d'une implantation, cohérence entre vues).

Le cours commence par une brève introduction à UML et à Z, se poursuit par une présentation détaillée de l'intégration des annotations Z dans le diagramme de classes et l'illustration sur des études de cas du processus de spécification et de l'utilisation des outils associés.

Yves Ledru est Professeur à l'Université Joseph Fourier de Grenoble et au laboratoire LSR/IMAG. Il y enseigne le Génie Logiciel et les méthodes formelles (en particulier VDM et Z). Ses recherches portent sur l'application de méthodes formelles à divers stades du développement de logiciels (ingénierie des exigences, architecture logicielle, test). Cette application passe notamment par une intégration de ces méthodes avec UML.