Implémentation JAVA d'une spécification B. Application aux bases de données
Cet article décrit une démarche complète et outillée de développement d'applications bases de données sûres. Le point de départ est une spécification B obtenue en traduisant des diagrammes UML dotés d'une sémantique formelle dédiée aux systèmes d'information. Cette spécification est ensuite raffinée par des règles automatiques et prouvées afin de rendre la spécification finale proche d'une implémentation relationnelle de telle sorte que la dernière phase de traduction soit intuitive et naturelle. La contribution principale de ce papier est de fournir une démarche systématique de traduction des composants terminaux B en une implémentation relationnelle. Cette traduction concerne deux aspects complémentaires : les données concrètes correspondant au schéma de la base de données, et les opérations concrètes B correspondant aux différents traitements. Contrairement à un schéma de bases de données qui peut être entièrement défini en SQL, les traitements nécessitent l'utilisation d'un langage hôte offrant des structures de contrôle équivalentes aux constructeurs de substitutions B.
This article describes a complete and tool-supported approach for the development of safe database applications. The starting point of our approach is a B specification obtained from UML diagrams for which a formal semantics, dedicated to information systems, is assigned. This specification is then refined by formal and proved rules to make the final specification close to a relational implementation such that the last translation phase is intuitive and straightforward. The main contribution of this article is to provide a systematic approach translating the terminal B components into a relational implementation. This translation concerns two complementary aspects: the data corresponding to the database schema, and the B operations corresponding to the system functionalities. Contrary to a database schema which can be completely defined in SQL, functionalities require the use of a programming language offering control structures which should be equivalent to B substitution constructors.
A.MAMMAR, R.LALEAU
Reçu le 8 décembre 2005.
Accepté le 6 juillet 2006.
aide au développement, bases de données, raffinement, codage.
development assistance, databases, refinement, coding.
Français
|
