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 21/8 - 2002  - pp.1099-1120
TITRE
Automatiser les preuves d'un sous-langage de la méthode B

RÉSUMÉ
Cet article propose une méthode pour automatiser les preuves pour un sous-langage de la méthode B, en utilisant un prouveur dédié. Nous définissons d’abord le langage, puis exposons la stratégie du prouveur associé, et son implantation au sein de l’Atelier B. Nous étudions ensuite les propriétés du prouveur. Un exemple réel d’application industrielle est exposé pour illustrer le processus.

ABSTRACT
This article illustrates the automatisation of proofs for a sub-language of the B method, by using a dedicated prover. First, we define the language, then we explain the strategy of its prover, and the implementation within the tool Atelier B. Next, we study the properties of the prover. A real example of industrial application is exposed to illustate the process.

AUTEUR(S)
Olivier BOITE

MOTS-CLÉS
preuve automatique, méthode B, vérification d’invariants ferroviaires.

KEYWORDS
automatic proof, B method, railway interlocking verification.

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  (148 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier