Tous nos rayons

Déjà client ? Identifiez-vous

Mot de passe oublié ?

Nouveau client ?

CRÉER VOTRE COMPTE
Spécification formelle avec B

Librairie Eyrolles - Paris 5e
Indisponible

Spécification formelle avec B

Spécification formelle avec B

Henri Habrias

414 pages, parution le 01/09/2001

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 01/09/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

Avantages Eyrolles.com

Livraison à partir de 0,01 en France métropolitaine
Paiement en ligne SÉCURISÉ
Livraison dans le monde
Retour sous 15 jours
+ d'un million et demi de livres disponibles
satisfait ou remboursé
Satisfait ou remboursé
Paiement sécurisé
modes de paiement
Paiement à l'expédition
partout dans le monde
Livraison partout dans le monde
Service clients 0 321 79 56 75 sav@commande.eyrolles.com
librairie française
Librairie française depuis 1925