Accueil -
Nouveautés -
Produit -
Versions -
Télécharger -
Manuels -
Maintenance -
Politique de Distribution
Perspectives & Appels à Contribution -
Support -
Formation -
Documents -
Presse -
Références -
R&D -
Contacts -
Emploi -
Liens -
Votre Compte
Documents sur B
Généralités
Titre |
Auteur |
Fichier |
B : Une méthode de développement de logiciels sûrs |
Loïc PELHATE |
|
Software Development with B (En Japonais) |
- |
Manuels de Référence
Titre |
Auteur |
Fichier |
|
Le manuel de référence du langage B 1.8.6 |
ClearSy |
|
|
La table des symboles du langage B 1.8.6 |
ClearSy |
Applications industrielles : automobile
Titre |
Auteur |
Fichier |
|
Les principes de fonctionnement formalisés (QSL) |
G. Pouzancre |
|
|
Modélisation en B événementiel des fonctions mécaniques, électriques et informatiques d'un véhicule (TSI) |
G. Pouzancre, J.P. Pitzalis |
|
|
How to diagnose a modern car with a formal B model (ZB'2003) |
G. Pouzancre |
|
|
Formalized operations principles |
D. Sabatier |
|
|
Conception générale formelle des sous-systèmes électroniques d'un véhicule - Le SPRAT - AFIS 2005 |
G. Pouzancre |
Applications Industrielles : Ferroviaire
Titre |
Auteur |
Fichier |
|
Approche Formelle pour la réalisation d'un système sécuritaire de contrôle commande de façades de quais - Coppilot - AFIS 2006 |
G. Pouzancre |
Applications industrielles : carte à puce
Voir en priorité le site de Gemplus à ce sujet. Quelques documents sont disponibles ci-dessous.
Titre |
Auteur |
Fichier |
|
Adaptable Translator of B Specifications to Embedded C Programs |
D. Bert, S. Boulmé, M-L. Potet, A. Requet, L. Voisin |
|
|
Formal Implementation of a Verification Algorithm using the B Method |
L. Casset |
|
|
Formal Development of an Embedded Verifier for Java Card Byte Code |
L. Casset |
|
|
Development of an embedded verifier for Java Card Byte Code using Formal Methods |
L. Casset |
|
|
Construction Correcte de Logiciels pour Carte à Puce |
L. Casset |
Modélisation de systèmes en B
Titre |
Auteur |
Fichier |
|
Guidelines to Formal System Studies |
J. R. Abrial |
|
|
Introducing Dynamic Constraints in B |
J. R. Abrial, L. Mussat |
|
|
Etude Système: méthode et exemple |
J. R. Abrial |
|
|
Le cahier des charges: contenu, forme et analyse |
J. R. Abrial |
|
|
Event Driven System Construction |
J. R. Abrial |
|
|
Event Driven Sequential Program Construction |
J. R. Abrial |
|
|
Event Driven Distributed Program Construction |
J. R. Abrial |
|
|
Event Driven Electronic Circuit Construction |
J. R. Abrial |
|
|
Event Model Decomposition |
J. R. Abrial |
|
|
CompoSys, un outil de modélisation des systèmes - AFADL'06 |
Florent Patin |
|
|
Application industrielle de la méthode formelle B - CEAT |
Thierry Servat |
|
|
Industrial Use of B |
ClearSy |
|
|
An overview of Atelier B 4.0 - Nantes 2008 |
Antoine Requet |
Exemples
Titre |
Auteur |
Fichier |
|
Etude de cas: distributeur de billets |
ClearSy |
|
|
Etude de cas: portrait robot |
ClearSy |
|
|
Etude de cas: contrôle d'accès à un bâtiment |
ClearSy |
|
|
Modèles Réactifs - Exemple de B Evénementiel "L'Ile" |
Louis Mussat |
Traducteur B Evenementiel / B
Titre |
Auteur |
Fichier |
|
Manuel de référence du B événementiel |
ClearSy |
|
|
Manuel utilisateur du traducteur |
ClearSy |
|
|
Traducteur (Logic Solver) |
ClearSy |
Guides d'Utilisation de B (Projet Matisse)
Titre |
Auteur |
Fichier |
|
MATISSE Handbook: Board Level storyboard |
ClearSy |
|
|
Project Manager's Handbook for System Construction |
ClearSy |
|
|
Practitioners Handbook |
ClearSy |
Programmation Logic Solver
Titre |
Auteur |
Fichier |
|
Manuel de syntaxe |
ClearSy |
|
|
Manuel de sémantique |
ClearSy |
|
|
Manuel de référence |
ClearSy |
|
