ACCUEIL

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

APPEL À
CONTRIBUTION
Décisions, argumentation et traçabilité dans l’Ingénierie des Systèmes d’Information
En savoir plus >>
Autres revues >>

Ingénierie des Systèmes d'Information

Networking and Information Systems
1633-1311
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 6/2 - 2001  - pp.41-72
TITRE
Développement formel par raffinement d’applications bases de données sûres

RÉSUMÉ

Cet article propose une approche formelle pour le développement d’applications bases de données sûres. Cette approche consiste en la génération d’une implémentation relationnelle à partir de spécifications formelles. On décrit préalablement l’application à l’aide de notations graphiques, puis un processus automatique est appliqué afin de les traduire en spécifications formelles B. En utilisant le processus de raffinement B, un ensemble de règles de raffinement, opérant sur les données et les opérations, est utilisé sur les spécifications ainsi obtenues. Ces phases de raffinement ont pour but de rendre les spécifications finales proches du langage d’implémentation cible choisi, de telle sorte que la dernière phase de codage devienne intuitive et naturelle. De manière générale, le processus de raffinement est une tâche manuelle, relativement coûteuse, en particulier en phase de preuve. Grâce au caractère générique de ces règles de raffinement, un outil de raffinement assisté peut être réalisé, permettant ainsi la réduction du coût du processus de raffinement.

ABSTRACT

This article proposes a formal approach for developing safety database applications. This approach consists of generating relational database implementations from formal specifications. We begin by designing the application with graphical notations such as UML, OMT... then an automatic process is used to translate them into B formal specifications. Using the B refinement process, a set of refinement rules, acting on both data and operations (programs), are applied on the specifications. These refinement phases aim at producing a final B specification close to the chosen target language implementation such that the last step of the coding becomes more intuitive and straightforward. The refinement process is generally a manual and very costly task especially in proof phase. Thanks to the generic feature of the refinement rules, an assistant refiner can be elaborated, allowing the cost of the refinement process to be reduced.

AUTEUR(S)
Amel MAMMAR

MOTS-CLÉS
applications bases de données, méthode formelle b, processus de raffinement,

KEYWORDS
database applications, b formal method, refinement process, proofs.

LANGUE DE L'ARTICLE
Français

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



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier