Overview   Tree   Domains   Index 
Bibliography
PREV  NEXT FRAMES  NO FRAME 

[RBS+96]  Les apports de la preuve en B

Roques.fmlm96 (In proceedings)
Author(s)Roques, Clément and Bustany, François and Sabatier, Denis
Title« Les apports de la preuve en B »
InColloque fiabilité et Maintenabilité Lambda-Mu 10
Page(s)12
Year1996
AddressSt-Malo, France.

Abstract
B est une méthode de spécification formelle actuellement utilisée dans la réalisation de logiciels critiques de sécurité. En particulier, B est un langage de spécification, conception et réalisation du logiciel de conduite automatique de métros de la nouvelle ligne METEOR de la RATP. Dans cet article nous montrons quels sont les apports des démonstrations mathématiques de B dans le cadtre d'un processus industriel de production de systèmes intégrant des composants logiciels. Nous verrons comment l'utilisation d'un système formal tel que B assure la correction du logiciel produit à sa spécification abstraite en permettant la validation par preuves mathématiques.

BibTeX code
@inproceedings{Roques.fmlm96,
  month = oct,
  author = {Roques, Cl{\'e}ment and Bustany, Fran{\c{c}}ois and Sabatier,
            Denis},
  booktitle = {Colloque fiabilit{\'e} et Maintenabilit{\'e} Lambda-Mu 10},
  domains = FORMAL:B,
  title = {Les apports de la preuve en {B}},
  address = {St-Malo, France.},
  year = 1996,
  pages = {12},
}

Documents in the same domains
- Root
\- Formal Specification/The Method B
+ [BW+96] Butler M. et al., "Distributed Systems Development in B" (1996)
\ [RBS+96] Roques C. et al., "Les apports de la preuve en B" (1996)
 Overview   Tree   Domains   Index 
Bibliography
PREV  NEXT FRAMES  NO FRAME 

Submit a bug

This document was generated by bib2html 4.0.
Copyright © 1998-05 Stéphane GALLAND (under the GNU General Public License)

Valid HTML 4.01!Valid CSS!