Spécification formelle avec B

Henri Habrias

414 pages, parution le 05/10/2001

Ajouter à une liste

Expédié sous 9 jours

Livraison à partir de 0,01€ dès 35€ d'achats
Pour une livraison en France métropolitaine

QUANTITÉ

Résumé

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.

Spécification formelle avec B 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.

A partir d'exemples simples de spécifications, l'ouvrage 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.

Sommaire

1. Les sources de B
2. Re-rédaction d'un cahier des charges et introduction au concept de machine abstraite
3. Introduction au développement d'un logiciel en B par un exemple
4. La logique de la preuve
5. Ensembles
6. Relations et fonctions
7. Objet mathématique. nombres naturels, suite, arbres
8. Structure d'une machine abstraite et preuve d'opération
9. Les substitutions
10 :Choix de modèlisations ensemblistes
11. L'approche base de données, les contraintes dynamiques et l'hypothèse du déterminisme linguistique de Sapir- Whorf
12. Le raffinage
13. Séquencement et boucle
14. Composition des machines et des raffinements
16. l'implantation finales et la structure d'un projet B
17. B évènementiel
18. B,VDM,Z et Spécifications algébriques
19. Glossaire
20. Bibliographie

L'auteur - Henri Habrias

Henri Habrias est professeur a l'universite de Nantes. Il enseigne le genie logiciel aux etudiants en IUT, en DEA et DESS. Il est responsable de l'equipe Methodes et specifications formelles de l'Institut de recherche en informatiques de Nantes (IRIN).

Caractéristiques techniques

	PAPIER
Éditeur(s)	Hermès - Lavoisier
Auteur(s)	Henri Habrias
Parution	05/10/2001
Nb. de pages	414
Format	15,5 x 23,5
Couverture	Broché
Poids	624g
Intérieur	Noir et Blanc
EAN13	9782746203020
ISBN13	978-2-7462-0302-0