Automatic generation of reliable components from B formal specifications
Génération automatique de composants logiciels sûrs à partir de spécifications formelles B
Résumé
These works are related to the study of the code generation from B formal specifications. The main aspect that should be studied in the code generation is the modularity of the B language. We have expressed the B modularity with an Harper-Lillibridge-Leroy module system (an ML-like module system). This modelisation clarifies some aspects of the B modularity and gives us a representation of the B modules that are used during the phase of code generation. This new module system for the B language allows us to tackle a software production technique: the components based approach. This technique is often used conjointly with the design by contracts technique. Our code generation process allows to blend the design by contracts approach, the component based approach and the B method. We can take advantage of the three approaches to develop software.
Ce mémoire est consacré à l'étude de la génération de code à partir de spécifications formelles B. L'aspect primordial à maîtriser pour la génération de code est la modularité du langage B. Pour ce faire, nous avons modélisé le système de modules du langage B en l'exprimant par un système de modules à la Harper-Lillibridge-Leroy. Cette modélisation nous permet de clarifier certains aspects de la modularité de B et nous permet ainsi d'avoir une représentation des spécifications B qui pourra ensuite être utilisée lors de la phase de génération de code. Ce nouveau système de module pour B nous permet également d'aborder une technique de production de logiciel, la programmation par composants. Cette technique est souvent utilisée conjointement à la programmation par contrats. Notre démarche de génération de code permet de marier ces deux techniques à celle du développement formel B pour tirer partie des avantages de chacune des méthodes de développement.
Origine : Fichiers produits par l'(les) auteur(s)