Un format fédérateur pour l'évaluation de spécifications formelles en Programmation Logique avec Contraintes
Cet article définit une représentation intermédiaire pour l'évaluation à contraintes de spécifications formelles logico-ensemblistes en particulier pour les notations B et Z. Cette représentation intermédiaire est une réécriture de la spécification formelle en un format prédicatif avant-après. Elle permet de décrire toute spécification formelle B ou Z en un système de contraintes équivalent. Cette traduction s'effectue au moyen d'une procédure spécifique permettant d'optimiser l'évaluation des comportements du modèle formel. L'autre intérêt de ce format est d'offrir un langage d'entrée unique à l'environnement de génération de tests fonctionnels aux limites BZ-Testing-Tools. Cet environnement a déjà été utilisé dans le cadre de projets industriels qui ont pu ainsi valider ses différents composants.
The article defines an intermediate form to constrained evaluation of formal model described in language B and Z. The intermediate form is a rewritten of formal specification to before-after predicate form. It allows to rewrite all formal B and Z specification into constraints system. The translation step allows to optimize the constrained evaluation of behavior of the model. Another interest of the form is to give up only one language as an input of the BZTesting-Tools environment tools. The BZ-Testing-Tools is a set of tools to generate functional limit test. It was used in different industrial case studies.
Méthodes formelles, évaluation à contraintes, notation B, animation, génération de tests.
Formal methods, constrained evaluation, B notation, animation, test generation.
Français
|
