Verification and Correction of B Specification in a CBSE approach
Vérification et correction des spécifications B : application à l'assemblage de composants
Résumé
The subject of our thesis aims at studying the verification and the correction of B specifications in the context of a CBSE approach. The B method is recognized as a well equipped formal method, used for developping software formally. It is characterized by a refinement capability and a power of provers, and thus allows a rigorous development. The CBSE approach consists in developping software by components assembly ; it finds its interest for large complicated systems. Our research provides three main contributions. The first contribution deals with some B constructions based on the refinement and the inclusion of B machines. Indeed, we study these B constructions for the specification of relations between labelled transition systems. The second contribution consists of the use of two formalisms : (i) the UML formalism to specify the assembly of two interfaces (required and provided) and of several components as well as the communications betweeen the components ; (ii) the B formalism to verify the assemblies. The third contribution studies the correction of the B specification from the feedback of unsuccessful proofs. This study is also generic and independent of the context, then it takes into consideration the CBSE context and it is interested in the detection and the correction of the incompatibilities : for the assembly of two interfaces we correct the adapters by considering the syntactic, semantics and protocol levels, while for the assembly and the coordination of several components we correct the mediators by considering the syntactic and protocol levels.
Le sujet de cette thèse est l'étude de la vérification et de la correction de spécifications B dans le contexte d'une approche CBSE ("Component-Based Software Engineering"). La méthode B est reconnue comme une méthode formelle bien outillée pour développer formellement des logiciels, elle dispose du raffinement et de prouveurs permettant un développement rigoureux. L'approche CBSE consiste à développer des logiciels par assemblage de composants, elle trouve son intérêt pour des systèmes de grandes tailles. Cette thèse comprend trois contributions principales. La première est la mise en évidence de schémas de constructions B basés sur le raffinement et l'inclusion de machines B ainsi que l'étude de ces schémas pour modéliser des relations entre des Systèmes de Transitions Etiquetés (STEs). La deuxième contribution consiste en l'utilisation de deux formalismes : (i) le formalisme UML pour spécifier l'assemblage de deux interfaces (fournie et requise) et de plusieurs composants ainsi que les communications entre composants, (ii) le formalisme B pour vérifier les assemblages. La troisième contribution étudie l'aide à la correction des spécifications B à partir de l'échec de la preuve en B. Cette étude est d'abord générale et indépendante du contexte, puis elle tient compte du contexte CBSE et s'intérresse à la détection et la correction des incompatibilités : pour l'assemblage de deux interfaces, on corrige les adaptateurs en considérant les trois niveaux syntaxique, sémantique et protocole, pour l'assemblage et la coordination de plusieurs composants, on corrige les médiateurs en considérant les niveaux syntaxique et protocole.