Spécification formelle avec B

Auteur :

Langue : Français
Couverture de l'ouvrage Spécification formelle avec B

Thèmes de Spécification formelle avec B

Date de parution :
Ouvrage 414 p. · 16x24 cm · Broché
Retiré de la vente
ISBN : 9782746203020 EAN : 9782746203020
Hermes Science
La méthode B a été élaborée par Jean-Raymond Abrial pour spécifier, concevoir et coder des systèmes logiciels. Elle est utilisée dans l'industrie, notamment dans les systèmes de sécurité, de protection et de contrôle de vitesse des trains. Cet ouvrage est une introduction à la notation B et à la méthode B. Le concept de base est celui de machine abstraite dont l'état est décrit par un invariant. La méthode consiste à prouver formellement que les opérations respectent bien l'invariant, puis à raffiner les machines abstraites en machines implantables, et à prouver que ce raffinage est correct. Le logiciel est ainsi prouvé par construction relativement à sa spécification. L'architecture du logiciel préconisée est l'architecture en couche. À partir d'exemples simples de spécifications, ce livre propose un développement complet en B. Il présente les bases mathématiques et logiques mises en oeuvre et détaille les éléments du langage B, en allant de la spécification à l'implantation.
Les services de B. Rerédaction d'un cahier des charges et introduction au concept de machine abstraite en B. Introduction au développement d'un logiciel en B par un exemple. Logique et preuve. Ensembles. Relations et fonctions. Objets mathématiques : nombres naturels, suites, arbres. Structure d'une machine abstraite et preuve d'opération. Les substitutions. Choix de modélisations ensemblistes. L'approche bases de données, les contraintes dynamiques, l'hypothèse du déterminisme linguistique de Sapir-Whorf et quelques autres propos. Le raffinage. Séquencement et boucle. Composition des machines et des raffinements. L'implantation finale et la structure d'un projet B. B événementiel. B, VDM, Z et spécifications algébriques. Glossaire B. Notation "mathématique" et notation ASCII pour spécifier B.