ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Autres revues >>

L'Objet

1262-1137
logiciel, bases de données, réseaux
Publication abandonné
 

 ARTICLE VOL 9/4 - 2003  - pp.75-94  - doi:10.3166/objet.9.4.75-84
TITLE
Temporal Logic Verifications for U M L

RÉSUMÉ
Une difficulté bien connue concernant la vérification de propriétés en UML est le besoin de formalisation. Puisqu'UML permet à la fois la spécification des types de données et des comportements dynamiques, la vérification de propriétés logiques fait également apparaître d'autres problèmes, notamment la possibilité de système de transition de taille infinie. Cet article présente un exemple de système spécifié en UML et complété avec une approche formelle et orientée composant. Nous utilisons une approche algébrique, appelée Type Abstrait Graphique (TAG) et basée sur un Statechart et une spécification de type abstrait partiel. Nous montrons qu'il est alors possible d'écrire et de prouver des propriétés de logique temporelle dans ce contexte. Du fait de l'utilisation des Statecharts, i.e. des systèmes symboliques avec des gardes, des variables et des types de données, le recours à la vérification de modèle classique n'est pas suffisante. Nous préconisons de réaliser les preuves avec un démonstrateur général et l'utilisation d'opérateurs fonctionnels exprimant le temps logique. Nous montrons plusieurs exemples de propriétés et de preuves réalisées en logique du premier ordre.


ABSTRACT
To verify UML specifications, one needs formal specifications which is a well-known difficulty. Since UML allows both the use of data types and dynamic specifications, the verification of temporal logic properties leads to other problems such as unbound labelled transitions systems. This paper presents an example of a system specified in UML and completed with a formal and component-oriented approach. We use an algebraic approach called Graphic Abstract data Types (GAT) based on Statecharts and algebraic specifications of partial abstract data types. We show that writing and proving temporal logic properties in such a context is possible. Because we have Statecharts: i.e. a symbolic system with guards, variables and data values, classical model checking is not sufficient enough. We rather advocate proofs with a general theorem prover and the use of functional operators expressing logical time. We show several examples of properties and proofs using first-order predicate logic.


AUTEUR(S)
Jean-Claude ROYER

MOTS-CLÉS
Type abstrait algébrique, architecture, composant, logique du premier ordre, spécification formelle, Larch Prover, preuve, propriété temporelle, UML.

KEYWORDS
Abstract Data Type, Architecture, Component, First-Order Logic, Formal Specification, Larch Prover, Proof, Temporal Property, UML.

LANGUE DE L'ARTICLE
Anglais

 PRIX
• Abonné (hors accès direct) : 34.95 €
• Non abonné : 34.95 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (192 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier