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.115-134  - doi:10.3166/objet.9.4.115-134
TITLE
Theorem Proving Support for View Consistency Checking

RÉSUMÉ
Cet article présente une approche formelle et automatisée pour la vérification de la cohérence des contraintes entre deux vues d'un système orientée objets. Les vues, décrites dans le langage de modélisation BON, capturent l'architecture statique du système grâce à des diagrammes de classes annotés par des contrats, la vue dynamique est réalisée par des diagrammes de collaboration. Les contraintes sont spécifiées comme une extension du métamodèle de BON et sont implémentées en PVS. Elles assurent que les séquences de messages qui apparaissent dans la vue dynamique sont légales compte tenu des pré-post conditions de la vue statique. Un exemple d'utilisation du prouveur PVS pour démontrer la cohérence des vues est décrit.


ABSTRACT
A formal, mechanically checked specification of the consistency constraints between two views of object-oriented systems are presented. The views, described in the BON modelling language, capture the static architecture of systems via contract-annotated class diagrams, and the dynamic view provided by collaboration diagrams. The constraints are specified as an extension of the BON metamodel, and are implemented in PVS. They ensure that the sequence of messages appearing in the dynamic view is legal, given the pre- and postconditions of methods appearing in the static view. An example of how the PVS theorem prover might be used to verify view consistency is described.


AUTEUR(S)
Richard F. PAIGE, Jonathan S. OSTROFF, Phillip J. BROOKE

MOTS-CLÉS
cohérence des vues, métamodélisation, démonstration, contrat, BON, PVS.

KEYWORDS
view consistency, metamodelling, theorem proving, BON, PVS.

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  (142 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier