ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 23/7 - 2004  - pp.855-878  - doi:10.3166/tsi.23.855-878
TITRE
Validation des règles de base de l'Atelier B

RÉSUMÉ
La méthode B permet de construire par raffinement un programme correct à partir d'une spécification abstraite qui exprime les besoins. Chaque étape de raffinement est validée à condition que soient établies certaines propriétés. La preuve de ces propriétés se fait à l'aide d'un outil de preuve, le prouveur de l'Atelier B par exemple. Ce dernier utilise des tactiques de preuve et des règles de base. Notre objectif est de valider les règles de base de l'Atelier B. Ces règles ont été validées manuellement par le passé. Pour plus de confiance, nous avons choisi de les valider formellement, à l'aide du système Coq. L'article propose une formalisation en Coq d'un sous-ensemble du langage B. Nous proposons ensuite une méthode de validation des règles de base de l'Atelier B ou plus exactement d'un sous-ensemble bien choisi de ces règles.

ABSTRACT
The B method enables us to build a correct program from an abstract specification expressing the requirements, by refining step by step the abstract specification. Each step must be validated by proof with the help, for example, of the Atelier B proof tool. The Atelier B proof tool uses proof tactics and basic rules. Several years ago, experts proved these rules manually. Our objective is to validate the basic rules in a formal way. This article provides a formalization of a subset of the B language within the Coq system. Then we propose a methodology to validate the basic rules of the Atelier B or more precisely a convenient subset of these rules.

AUTEUR(S)
Karim BERKANI, Catherine DUBOIS, Alain FAIVRE, Jérôme FALAMPIN

Reçu le 7 avril 2003.    Accepté le 19 janvier 2004.

MOTS-CLÉS
validation, preuve formelle, théorie des ensembles, théorie des types, Atelier B, règles de base, Coq.

KEYWORDS
validation, formal proof, set theory, type theory, Atelier B, basic rules, Coq.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (241 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier