B : passé, présent, futur, Jean-Raymond Abrial, TSI, 1 February 2003
B : passé, présent, futur
Abstract
Cet
article est une presentation non technique, mais rigoureuse, de la
methode B. Il s'adresse aux lecteurs qui ont entendu parler de B et qui
souhaitent en savoir davantage. Il indique quelle est la demarche
initiale de B et sa raison d'etre, c'est-a-dire la modelisation de
logiciels et plus generalement des systemes. Il precise ensuite ce
qu'est un modele et decrit les concepts importants de la methode, a
savoir le raffinement, la decomposition et la genericite. La methode B
permet d'envisager les modeles sous deux aspects: la vision locale et la
vision globale. Le deuxieme aspect utilise une nouvelle facon d'ecrire
le B, appelee B-evenementiel. La correction des logiciels produits par
la methode B est assuree par des preuves mathematiques. L'article
explique ce que signifie prouver et quand ces preuves doivent etre
faites. Enfin, il indique comment integrer B dans le contexte industriel
pour la construction de systemes operationnels. L'article est illustre
par quelques exemples informels, tires da la pratique de B.
Comments
Post a Comment