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 22/1 - 2003  - pp.89-118  - doi:10.3166/tsi.22.89-118
TITRE
B : passé, présent, futur

RÉSUMÉ
Cet article est une présentation non technique, mais rigoureuse, de la méthode B. Il s'adresse aux lecteurs qui ont entendu parler de B et qui souhaitent en savoir davantage. Il indique quelle est la démarche initiale de B et sa raison d'être, c'est-à-dire la modélisation de logiciels et plus généralement des systèmes. Il précise ensuite ce qu'est un modèle et décrit les concepts importants de la méthode, à savoir le raffinement, la décomposition et la généricité. La méthode B permet d'envisager les modèles sous deux aspects : la vision locale et la vision globale. Le deuxième aspect utilise une nouvelle façon d'écrire le B, appelée "B-événementiel". La correction des logiciels produits par la méthode B est assurée par des preuves mathématiques. L'article explique ce que signifie "prouver" et quand ces preuves doivent être faites. Enfin, il indique comment intégrer B dans le contexte industriel pour la construction de systèmes opérationnels. L'article est illustré par quelques exemples informels, tirés da la pratique de B.


ABSTRACT
This paper is a non technical, yet rigorous, presentation of the B method. It is intended to be read by people who know a little about B and want to know more. It first presents the main approach of B, its raison d'être, namely the construction of models of software and more generally of discrete systems. It then makes precise what is meant by a "model", and also describes the important concepts at work in this approach, namely those of refinement, decomposition, and genericity. In applying B, two broad kinds of models are envisaged: those devoted to a "local" vision and those devoted to a "global" one. The second vision uses a new approach in writing B models, which is called "Event B". The correctness of programs written thanks to B are enforced by using formal proofs. It is explained what it means to "prove" a model and also how such proofs can be performed in practice. Finally, the paper shows how such an approach can be incorporated within an industrial environment in order to build operational systems. A number of practical examples illustrates the various facets presented in the paper. Modélisation, construction de logiciels et de systèmes, vérification de propriétés,


AUTEUR(S)
Jean-Raymond ABRIAL

MOTS-CLÉS
méthode B.

KEYWORDS
Modelisation, software and system construction, property verification, B method.

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



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier