Un environnement formel pour le développement d'applications bases de données
Institution:
Paris, CNAMDisciplines:
Directors:
Abstract EN:
This work presents 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 process is generally a manuel and very costy task especially in proff phase. Thanks to the generic feauture of the refinement rules, an assistant refiner can be elaborated, allowing the cost of the refienement process to be reduced.
Abstract FR:
Ce travail présente 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 UML, puis un processus automatique est appliqué afin de les traduire en spécifications B. En utilisant le processus de raffinement, un ensemble de règles de raffinement; opérant sur les données et les opérations, est utilisé sur les spécifications obtenues. Ces phases de raffinement ont pour but de rendre les spécifications proches du langage d'implémentation cible choisi, la dernière phase de codage devient intuitive et naturelle. De manière générale, le raffinement est manuel, relativement coûteux, 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 la réduction du côut du processus de raffinement.