QSL: Autour d'UML

Séminaire QSL du Pôle ``Intelligence Logicielle'' du LORIA

Autour d'UML

27 mars 2003

LORIA
Salle B013
LORIA, Campus Scientifique
Vandoeuvre-les-Nancy
(directions)

Programme : Jeanine Souquières

Le but de cette journée est de présenter différents travaux actuels autour du langage UML et des méthodes formelles.
9h45 Bienvenue

Registration expired

10h00 Test intégré dans des composants logiciels dérivés d'UML
Frank Barbier, LIUPPA, Université de Pau
Cet exposé présente les résultats du projet européen Component+ (IST 1999-20162). On s'intéresse spécifiquement aux composants logiciels sur étagère (COTS components) et à leur processus d'acquisition. En tant que structures fermées (encapsulation), un blocage réside dans la confiance dans de tels composants : ils ne sont pas ou peu spécifier et donc intelligibles avec difficulté, la prédiction de leurs comportements (« sémantique » de leur fonctionnement, de leur potentiel de collaboration/échange avec des composants tiers, contrats qu'ils sont en mesure de respecter) et la connaissance de leur qualité de service (temps de réponse, encombrement de ressources, aptitude au déploiement rapide) ne sont envisageables que si leur conception l'a prévu. Le test intégré vise donc à instrumenter le code pour évaluer in-situ les COTS composants. La contribution consiste essentiellement en une technique de conception fondée sur des Statecharts UML où il existe une bijection entre code et spécification : idée de spécification exécutable. Les acquéreurs bénéficient alors de modèles didactiques avec lesquels ils peuvent « jouer » dans leurs environnements réels d'exécution. Une libraire Java nommée BIT/J supporte cette démarche. Utilisant le modèle de composants JMX (Java Management Extensions) généralisant le concept de « manageable component » ou MBean, il devient alors possible de tester les composants à distance, de piloter les composants (« monitoring ») et par conséquent, piloter la machine d'état embarquée dans le composant. Une démonstration de cette librairie sera faite à la fin de l'exposé.

11h00 Pause

11H20 RoZ, un outil intégrant UML et Z pour la modélisation des systèmes d'information
Yves Ledru, (LSR/IMAG) Grenoble
Les notations graphiques semi-formelles, comme UML, constituent aujourd'hui l'un des outils majeurs de modélisation des systèmes informatiques. De tels langages offrent une notation intuitive qui facilite la communication entre l'analyste et son client. Cependant, leur pouvoir d'expression reste limité et leur sémantique n'est pas totalement définie. L'intégration de telles notations avec des méthodes formelles permet d'améliorer la précision des spécifications et d'exploiter des outils de simulation, de test ou de vérification qui contribuent à la validation des spécifications. Notre équipe a ainsi développé l'outil RoZ qui intègre des annotations en Z au diagramme de classes d'UML. Cette intégration a plusieurs avantages:
elle précise la sémantique d'UML et augmente son expressivité,
elle apporte un guide méthodologique pour l'identification des contraintes exprimées par les annotations,
elle permet la génération automatique des spécifications de certaines opérations,
elle permet la validation formelle de certaines propriétés à l'aide d'un démonstrateur automatique.

12h30 Repas (individuel, peut être pris dans le restaurant du LORIA)

13h45 Utilisation de UML et B pour la production d'implémentations relationnelles
Régine Laleau, IEE, CNAM, Paris
Dans le domaine des systèmes d'information, les données sont traditionnellement modélisées de manière formelle et à un haut niveau d'abstraction en utilisant les modèles de type Entité/Association ou relationnel binaire. En revanche, la description des fonctionnalités reste relativement informelle. Un premier objectif des travaux de recherche de notre équipe a été de spécifier le comportement fonctionnel des transactions d'un SI au même niveau d'abstraction que les données, en utilisant une méthode de spécifications formelles existante afin de pouvoir bénéficier de tous les outils de raisonnement associés. On obtient ainsi une spécification globale d'un SI dont la cohérence données-traitements est vérifiée. Ensuite, nous avons montré qu'il était possible d'aller plus loin en générant, par un processus de raffinement, une implémentation relationnelle à partir de la spécification formelle obtenue. Le processus étant formel, les transactions générées sont correctes par rapport à la spécification. La méthode proposée est le résultat de la combinaison des notations graphiques UML avec la méthode formelle B dont le paradigme de spécification, basé sur les transitions d'états, est bien adaptée aux types de systèmes et aux types de propriétés considérés.

14h45 Intégration de données formelles dans les diagrammes d'états. Application aux diagrammes d'état d'UML
Pascal Poizat, Lami, Université d'évry, Val d'Essonne
Faire cohabiter génie logiciel et méthodes formelles de façon pragmatique permet de tirer le meilleur parti des deux approches : concepts puissants de structuration des spécifications, notations graphiques, expressivité et simplicité d'utilisation côté génie logiciel, définition claire et non ambiguë, abstraction, cohérence de vues, critères << de confiance >>, et vérification côté spécifications formelles. Depuis quelques années, nos travaux s'intéressent aux spécifications de composants formels mixtes, c'est-à-dire des spécifications réutilisables comportant plusieurs aspects tels que les aspects statiques (données, opérations), dynamiques (comportements, réactivité) et architecturaux (structure, synchronisation, communication, échange de valeurs). Après nous être intéressés à l'intégration de ces aspects dans les langages de spécification formels (LOTOS, SDL, Korrigan), et avoir remarqué de nombreux points communs, nous cherchons maintenant à proposer des << boîtes à outils >> formelles (sémantique opérationnelle et animation de spécifications, sémantique dénotationnelle, mécanismes de vérification et de génération de code) génériques pour ce cadre de composants formels mixtes. Dans cet exposé nous nous intéresserons plus particulièrement à la définition d'une sémantique opérationnelle générique permettant d'intégrer des techniques de spécification formelle pour les aspects statiques avec des langages de modélisation semi-formels pour les aspects dynamiques. Cette proposition se place à un niveau élevé d'abstraction puisqu'elle permet d'utiliser différentes sémantiques des diagrammes d'états (celles d'UML, des statecharts, de SDL par exemple). Notre approche est aussi souple et flexible puisqu'elle permet l'utilisation de différents langages de description des données (Z, B, spécifications algébriques), améliorant par là-même le niveau de réutilisabilité des spécifications. Nous aborderons tout d'abord les fondements formels de l'approche, puis nous l'illustrerons en l'appliquant à UML sur un exemple simple. Nous terminerons en montrant en quoi notre approche se différencie des approches existantes de combinaison et d'intégration de langages de spécification formels et semi-formels, basées généralement sur une traduction en Z ou en B.

15h20 Pause

15h45 Model Checking UML State Machines and Collaborations
Stephan Merz, INRIA Lorraine, LORIA, Nancy
The Unified Modelling Language (UML) provides many kinds of diagrams to specify different aspects of a system under development, which are useful at different phases of system design. Current UML editors provide only limited, syntactic means to ensure the consistency of the diagrams that represent a single system. In this talk I will present ongoing work, in collaboration with Alexander Knapp from the University of Munich, to apply model checking technology to validate UML state machines against interaction (collaboration or sequence) diagrams.

16h45 Fin de la journée

Registration expired

Jeanine Souquieres
Last modified: Tue April 01 16:45:42 MET 2003

Programme : Jeanine Souquières
Le but de cette journée est de présenter différents travaux actuels autour du langage UML et des méthodes formelles.
9h45	Bienvenue
Registration expired
10h00	Test intégré dans des composants logiciels dérivés d'UML Frank Barbier, LIUPPA, Université de Pau Cet exposé présente les résultats du projet européen Component+ (IST 1999-20162). On s'intéresse spécifiquement aux composants logiciels sur étagère (COTS components) et à leur processus d'acquisition. En tant que structures fermées (encapsulation), un blocage réside dans la confiance dans de tels composants : ils ne sont pas ou peu spécifier et donc intelligibles avec difficulté, la prédiction de leurs comportements (« sémantique » de leur fonctionnement, de leur potentiel de collaboration/échange avec des composants tiers, contrats qu'ils sont en mesure de respecter) et la connaissance de leur qualité de service (temps de réponse, encombrement de ressources, aptitude au déploiement rapide) ne sont envisageables que si leur conception l'a prévu. Le test intégré vise donc à instrumenter le code pour évaluer in-situ les COTS composants. La contribution consiste essentiellement en une technique de conception fondée sur des Statecharts UML où il existe une bijection entre code et spécification : idée de spécification exécutable. Les acquéreurs bénéficient alors de modèles didactiques avec lesquels ils peuvent « jouer » dans leurs environnements réels d'exécution. Une libraire Java nommée BIT/J supporte cette démarche. Utilisant le modèle de composants JMX (Java Management Extensions) généralisant le concept de « manageable component » ou MBean, il devient alors possible de tester les composants à distance, de piloter les composants (« monitoring ») et par conséquent, piloter la machine d'état embarquée dans le composant. Une démonstration de cette librairie sera faite à la fin de l'exposé.
11h00	Pause
11H20	RoZ, un outil intégrant UML et Z pour la modélisation des systèmes d'information Yves Ledru, (LSR/IMAG) Grenoble Les notations graphiques semi-formelles, comme UML, constituent aujourd'hui l'un des outils majeurs de modélisation des systèmes informatiques. De tels langages offrent une notation intuitive qui facilite la communication entre l'analyste et son client. Cependant, leur pouvoir d'expression reste limité et leur sémantique n'est pas totalement définie. L'intégration de telles notations avec des méthodes formelles permet d'améliorer la précision des spécifications et d'exploiter des outils de simulation, de test ou de vérification qui contribuent à la validation des spécifications. Notre équipe a ainsi développé l'outil RoZ qui intègre des annotations en Z au diagramme de classes d'UML. Cette intégration a plusieurs avantages: elle précise la sémantique d'UML et augmente son expressivité, elle apporte un guide méthodologique pour l'identification des contraintes exprimées par les annotations, elle permet la génération automatique des spécifications de certaines opérations, elle permet la validation formelle de certaines propriétés à l'aide d'un démonstrateur automatique.
12h30	Repas (individuel, peut être pris dans le restaurant du LORIA)
13h45	Utilisation de UML et B pour la production d'implémentations relationnelles Régine Laleau, IEE, CNAM, Paris Dans le domaine des systèmes d'information, les données sont traditionnellement modélisées de manière formelle et à un haut niveau d'abstraction en utilisant les modèles de type Entité/Association ou relationnel binaire. En revanche, la description des fonctionnalités reste relativement informelle. Un premier objectif des travaux de recherche de notre équipe a été de spécifier le comportement fonctionnel des transactions d'un SI au même niveau d'abstraction que les données, en utilisant une méthode de spécifications formelles existante afin de pouvoir bénéficier de tous les outils de raisonnement associés. On obtient ainsi une spécification globale d'un SI dont la cohérence données-traitements est vérifiée. Ensuite, nous avons montré qu'il était possible d'aller plus loin en générant, par un processus de raffinement, une implémentation relationnelle à partir de la spécification formelle obtenue. Le processus étant formel, les transactions générées sont correctes par rapport à la spécification. La méthode proposée est le résultat de la combinaison des notations graphiques UML avec la méthode formelle B dont le paradigme de spécification, basé sur les transitions d'états, est bien adaptée aux types de systèmes et aux types de propriétés considérés.
14h45	Intégration de données formelles dans les diagrammes d'états. Application aux diagrammes d'état d'UML Pascal Poizat, Lami, Université d'évry, Val d'Essonne Faire cohabiter génie logiciel et méthodes formelles de façon pragmatique permet de tirer le meilleur parti des deux approches : concepts puissants de structuration des spécifications, notations graphiques, expressivité et simplicité d'utilisation côté génie logiciel, définition claire et non ambiguë, abstraction, cohérence de vues, critères << de confiance >>, et vérification côté spécifications formelles. Depuis quelques années, nos travaux s'intéressent aux spécifications de composants formels mixtes, c'est-à-dire des spécifications réutilisables comportant plusieurs aspects tels que les aspects statiques (données, opérations), dynamiques (comportements, réactivité) et architecturaux (structure, synchronisation, communication, échange de valeurs). Après nous être intéressés à l'intégration de ces aspects dans les langages de spécification formels (LOTOS, SDL, Korrigan), et avoir remarqué de nombreux points communs, nous cherchons maintenant à proposer des << boîtes à outils >> formelles (sémantique opérationnelle et animation de spécifications, sémantique dénotationnelle, mécanismes de vérification et de génération de code) génériques pour ce cadre de composants formels mixtes. Dans cet exposé nous nous intéresserons plus particulièrement à la définition d'une sémantique opérationnelle générique permettant d'intégrer des techniques de spécification formelle pour les aspects statiques avec des langages de modélisation semi-formels pour les aspects dynamiques. Cette proposition se place à un niveau élevé d'abstraction puisqu'elle permet d'utiliser différentes sémantiques des diagrammes d'états (celles d'UML, des statecharts, de SDL par exemple). Notre approche est aussi souple et flexible puisqu'elle permet l'utilisation de différents langages de description des données (Z, B, spécifications algébriques), améliorant par là-même le niveau de réutilisabilité des spécifications. Nous aborderons tout d'abord les fondements formels de l'approche, puis nous l'illustrerons en l'appliquant à UML sur un exemple simple. Nous terminerons en montrant en quoi notre approche se différencie des approches existantes de combinaison et d'intégration de langages de spécification formels et semi-formels, basées généralement sur une traduction en Z ou en B.
15h20	Pause
15h45	Model Checking UML State Machines and Collaborations Stephan Merz, INRIA Lorraine, LORIA, Nancy The Unified Modelling Language (UML) provides many kinds of diagrams to specify different aspects of a system under development, which are useful at different phases of system design. Current UML editors provide only limited, syntactic means to ensure the consistency of the diagrams that represent a single system. In this talk I will present ongoing work, in collaboration with Alexander Knapp from the University of Munich, to apply model checking technology to validate UML state machines against interaction (collaboration or sequence) diagrams.
16h45	Fin de la journée
Registration expired