β-space : raffinement de descriptions architecturales en machines abstraites de la méthode formelle B
Institution:
ChambéryDisciplines:
Directors:
Abstract EN:
A software architecture describes its structure and behaviour using components and connectors, but their languages do not support the complete development of complex software systems, from architectural design to executable code. Some formal development methods permit to refine a software specification to obtain another one closer to the implementation, or even code, but without taking into account the system architectural description. We propose to use a refinement, mechanism to transform the architectural description into a "classical" formal specification, already supported by tools allowing the development achievement. We develop a formal system - named ß -SPACE - to bring successive refinements into operation, leading from the starting architectural description (in π-SPACE, a software architecture description language based on a process algebra) to a formal specification (a set of abstract machines of the B method, which is supported by tools to help the formal development and the code generation) to make a formal development of the application possible, in the B method framework, while guaranteeing that each refinement step preserves the initial architectural properties. The formal definition of the refinement is based on the rewriting logic, in which the abstract architectural and the target specification elements are represented. This logic is also supported by a tool which permits to automate the transformations. Our approach of the architectural refinement differs from other existing methods, by being interested not only in the addition of details to the formal description, but also in the transformation of its control structure: the composition of components and connectors in the architecture is transformed to obtain a hierarchy of B abstract machines. We ensure the conservation of the interesting architectural properties. This is an original approach both concerning its architectural range, its formalisation and its connection with the classical formal methods.
Abstract FR:
L'architecture d'un logiciel décrit sa structure et son comportement par des composants et des connecteurs, mais leurs langages n'autorisent pas le développement complet de systèmes logiciels complexes. Certaines méthodes de développement formel permettent de raffiner une spécification, pour en obtenir une autre plus proche de l'implémentation, voire du code, sans prendre en compte la description architecturale du système. Nous proposons d'utiliser un mécanisme de raffinement pour transformer la description architecturale en une spécification formelle "classique" disposant d'outils pour achever le développement. Nous développons un système formel ß-SPACE pour la mise en oeuvre de raffinements successifs, menant de la description architecturale de départ (en π-SPACE, langage de description d'architecture fondé sur une algèbre de processus) à une spécification formelle (ensemble de machines abstraites de la méthode B, qui dispose d'outils aidant au développement formel et à la génération du code) telle qu'un développement formel de l'application soit possible dans le cadre de la méthode B, en garantissant que chaque étape de raffinement conserve les propriétés de l'architecturale initiale. La définition formelle du raffinement est basée sur la logique de réécriture, pour représenter les éléments architecturaux abstraits et ceux du langage cible de spécification. Cette logique dispose d'un outil permettant d'automatiser les transformations. Notre approche du raffinement architectural diffère des méthodes existantes en s'intéressant en plus de l'ajout de détails à la description formelle à la transformation de sa structure de contrôle la composition de composants et de connecteurs de l'architecture est transformée pour obtenir une hiérarchie de machines abstraites B. Nous assurons la conservation des propriétés architecturales. C'est une approche originale à la fois sur sa portée architecturale sa formalisation et son articulation avec les méthodes formelles classiques.