B dans l industrie Utilisation de B événementiel

B dans l ’industrieB dans l ’industrie

Utilisation de B événementiel

application de B pourapplication de B pourproduire des systèmes sûrsproduire des systèmes sûrs

Prérequis initiaux

1er niveau de conception

Nième niveau de conception

niveau de décomposition

Spécification sous partieSpécification sous partie

niveaux de conception niveaux de conception

Traduction en code executable ou hardware

SYSTEME COMPLET

Preuves :•cohérence interne de chaque niveau•que chaque niveau N+1 répond aux prérequis du niveau N

En bleu : langage B

Atelier B : traducteurs C,C++,ADA

Atelier B : prouveur

Possibilité de limiterla partie formelleau niveau specs

détaillées

B une méthode formelle pourB une méthode formelle pour

le développement de logiciels sécuritaires ou de systèmes matériels sécuritaires

la rétro-ingénierie les études systèmes la validation de cahiers des charges

B est actuellement utilisé B est actuellement utilisé pourpour

Logiciels de Contrôles commandes (MTI, Alstom)

Validation de spécifications (PEUGEOT)

Validation / rétro-ingénierie de logiciels sécuritaires (MTI, Alstom)

Références industrielles Références industrielles (développement)(développement)

KVB, constructeur Gec-Alsthom Transport, client SNCF, 60.000 lignes B, 10 000 Preuves, 22 000 lignes Ada

Contrôle de vitesses, équipe 6000 trains depuis 93

CTDC, constructeur Gec-Alsthom Transport, client Le Caire / Calcutta, 5000 lignes B, 700 preuves, 3.000 lignes AdaContrôle/commande, équipe le métro du CAIRE et CALCUTA (91)

SAET METEOR, constructeur Matra Transport International, client RATP, 107 000 lignes B, 29 000 preuves, 87.000 lignes Ada Contrôle/commande embarqué dans le métro sans conducteur METEOR

B a aussi été étudié pourB a aussi été étudié pour

Temps-réel Protocoles de communication Automatismes industriels Conception d’application de gestion

avec données complexes

Description d'un système par Description d'un système par ses propriétésses propriétés B garantit que l'ensemble des

propriétés du système modélisé seront non contradictoires non ambiguës respectées par le système final

B apporte la formalisation du besoin la validation sans faille par la preuve la réutilisation la précocité de la détection des erreurs dans le

cycle de développement, absence de retour d ’anomalies

pour des besoins systèmes aussi bien que logiciels

Application de la Méthode BApplication de la Méthode B

On modélise en B des choix de réalisation du Système, certaines exigences.

Caractéristiques de la méthode description des propriétés d’un Système à l’aide d’un

formalisme mathématique, modulaire, hiérarchique : notion de raffinement validation par la preuve : debug systématique.

2 styles de B2 styles de B

B événementiel Les opérations représentent des événements

exemple : projet PEUGEOT

B « classique » les opérations représentent des services appelables

exemple : METEOR

2 types d ’application2 types d ’application

B système : Pour l ’analyse formelle des cahiers des charges Pour la conception d ’architecture des systèmes Ingénierie système souvent : B événementiel

B développement Pour la conception / développement de systèmes

informatiques Le code informatique est produit par traduction des

derniers niveaux de B (B0) souvent : B procédural

B événementiel pour les B événementiel pour les systèmessystèmes

prérequis pour l’ensemble du système :écrits comme les événements d’un modèle

design : raffinements B

decomposition

software sous project:prérequis (modèle B)

developpement

partie software

hardware sous project:prérequis (modèle B)

production hardware

hypothèses de contexteet conditions d’utilisation

(modèle B)

instructions d’emploiet restrictionspartie hardware

produit final

Utilisation de B en phase Utilisation de B en phase amontamont

succès duprojet preuve en phase

amont

A chacun son métierA chacun son métier

B système : qui pratique B ? Le spécialiste métier qui rédige les spécifications ?

Sûrement pas ! Le spécialiste métier se concentre sur son métier !

Spécialiste métier + expert formalisation Résultats toujours traduits en langage naturel

B développement : qui pratique B ? Le concepteur et le développeur...

2 organisations : Client + consultant ou sous traitance B (ex : PEUGEOT) Le client monte un pôle d ’experts B (ex : METEOR)

Evaluer BEvaluer B

B doit être employé avec des experts formaliser = conceptualiser ! débutant + B = programmation directe déguisée

Faire d ’abord des études pilotes examiner un sujet pour voir comment B pourrait s ’y

appliquer appliquer sur un sujet à taille réduite (1 ou 2 mois) :

étude pilote projet grandeur réelle

Eviter : évaluation par personne ne connaissant pas B seule

Mise en place d ’un Mise en place d ’un processus Bprocessus B mise en place en spirale :

évaluation

démarrage

projet pilote

projet taille réelle

Validation par la preuveValidation par la preuve

PreuvePreuveAutomatiqueAutomatique Examen des Examen des

lemmeslemmes

lemme lemme fauxfaux

PreuvePreuveInteractiveInteractive

100100%%

70 à 85%70 à 85%des lemmes des lemmes

justesjustes

15 lemmes / 15 lemmes / jourjour

Source Source BB

BUG

10%10%correctioncorrection

Génération Génération automatique de automatique de

lemmeslemmes

Validation par la preuveValidation par la preuve

Procédé non décidable Les vérifications faites par un compilateur sont

décidables application d ’un algorithme prédéfini qui aboutit

toujours Un prouveur applique un procédé non décidable

Avantages / inconvénients Aucune limite, tout problème peut se ramener à une

preuve Résolution non totalement automatisable

Pourquoi choisir B système ?Pourquoi choisir B système ?

Raisons économiques : Les imprécisions des spécifications coûtent cher

Avec B, peu de retours tardifs sur les spécifications éviter la phase de « flou » si coûteuse

Raisons organisationnelles Quand les spécifications ne disent rien, qui a raison ?

Avec B, aucun non dit, aucune ambiguïté

Se différencier : Quelle différence sur une expertise de spécifications ?

Utilisation d ’une formalisation mathématique intégrale

Analyse B pour suggérer des Analyse B pour suggérer des précisions précisions

Documents :spécifications techniques

STE STE STE

Interviews,contacts, notes

ModélisationsB

B

Demandes de précision

réponses

Rapport

Analyse B pour produire des Analyse B pour produire des documents formalisésdocuments formalisés


STE STE STE


ModélisationsB

Retraductionen français

BB


réponses

Analyse B et sûreté de Analyse B et sûreté de fonctionnementfonctionnement


STE STE STE


ModélisationsB

Arbresde défaillance,

AMDECBSdF


réponses

Analyse B et constitution Analyse B et constitution d ’arbres de dépannaged ’arbres de dépannage


STE STE STE


ModélisationsB

ArbresdépannageB

SdF


réponses

Outil externe

Pourquoi choisir un Pourquoi choisir un développement B ?développement B ? Raisons économiques :

Les tests coûtent beaucoup trop chers Avec B, il n'y a plus de tests unitaires Possible suppression des AEEL Plus de retour sur anomalies

Si on avait l ’intention de faire des tests...

Raisons sécuritaires : les erreurs peuvent avoir des conséquences

catastrophiques Avec B, il n'y a plus d'erreurs de conception et de

programmation

ConclusionConclusion

Avantages d ’une application B système procédé « léger » bras de levier important qualification élevée justifiée

Difficultés résultats avec B contre résultat d ’une analyse « bon

sens » B n ’est pas une justification, seul le résultat NECESSITE D ’ETRE HAUT NIVEAU : ABSTRACTION

savoir être haut niveau mais rester significatif

B événementiel pour les B événementiel pour les études systèmesétudes systèmes B procédural : force à être bas niveau B événementiel :

Doit être applicable facilement Doit permettre de rester haut niveau Ne doit pas être un nouveau langage de

programmation La preuve doit être « courante » Eviter les lourdeurs

Expertise de spécifications Expertise de spécifications avec Bavec B

vérification « à plat » de cohérence / complétude : exemple

PEUGEOT

Application de B à un Application de B à un niveau :niveau :mission STERIA chez mission STERIA chez PEUGEOTPEUGEOT

Documents : spécifications détaillées

STESTE

STESTE

STESTE


ModélisationsB

Retraductionen français

BB

Principes de fonctionnement formalisés

(PFF)

Application « 1 niveau »Application « 1 niveau »

Pas de raffinement : on modélise 1 niveau de détail pas de recherche d ’abstraction preuve simple de cohérence interne

Apports : Complétude Cohérence interne Disparition des ambiguïtés

Modélisation « 1 niveau »Modélisation « 1 niveau »

Application de B très accessible Règles :

Ne pas programmer. Le modèle doit être le reflet de la compréhension du fonctionnement, pas une pseudo-programmation de la fonction représentée.

Variables abstraites : une variable du modèle peut représenter une notion très abstraite, mais bien définie.

test : sur n ’importe quel scénario réel, le modélisateur doit savoir quelle est la valeur de la variable abstraite qui représente la situation observée.

Evénements : chaque opération B représente un instant précis dans le temps

Lecture des principes de Lecture des principes de fonctionnement formalisésfonctionnement formalisés

Exemple : fonction condamnation

Scénario choisiScénario choisi

T5, version supercondamnation Le véhicule est condamné (condamnation

simple) Une personne est à l ’intérieur, sur la

place avant conducteur Cette personne actionne la poignée

d ’ouverture de la porte conducteur : la porte s ’ouvre et le véhicule se déverrouille (override)

Quel est le détail de ce qui s ’est passé ?

1. Action poignée1. Action poignée

Evénement « Actionnement de la commande d ’ouverture intérieure », partie serrure dans le PFF fonction condamnation (PFF = principe de fonctionnement formalisé = retraduction du modèle B)

Effets indiqués : la serrure se déverrouille le pêne de la porte est libéré : la porte peut s ’ouvrir

2. Ouverture porte2. Ouverture porte

Evénement « Ouverture d ’une porte dont le pêne est libre », partie porte dans le PFF fonction condamnation (PFF = principe de fonctionnement formalisé = retraduction du modèle B)

Effets indiqués : l ’angle d ’ouverture devient non nul la position du pêne devient « ouvert » ou « premier

cran » le contacteur porte ouverte est fermé (il est asservi à

la position du pêne : pêne « ouvert » ou « premier cran » implique contact fermé)

3. Détection par BSI3. Détection par BSI

Evénement « Détection d ’une ouverture de porte avant », partie BSI dans le PFF fonction condamnation (PFF = principe de fonctionnement formalisé = retraduction du modèle B)

Effets indiqués : Si l ’état connu de la BSI est « condamnation simple »,

la BSI envoie l ’ordre de décondamnation (polarité + - - sur les trois fils de commande des 4 serrures)

Echo sur l ’écran, indication de l ’état déverrouillé sur la LED « état verrouillage »

Annulation de l ’interdiction d ’ouverture hayon

4. Déverrouillage centralisé4. Déverrouillage centralisé

Evénement « Arrivée d ’une commande sur une serrure », partie serrure dans le PFF fonction condamnation (PFF = principe de fonctionnement formalisé = retraduction du modèle B)

Effets indiqués : Les 3 autres serrures se déverrouillent

Points particuliersPoints particuliersvisibles dans le PFFvisibles dans le PFF Que se passe t-il si la serrure était en fait

super-condamnée ? Une serrure supercondamnée ne se décondamne pas

sur action de la poignée intérieure Donc pas d ’ouverture Donc aucune détection par la BSI

Et si la commande d ’ouverture EXTERIEURE de la porte était maintenue levée pendant ce temps ? l ’action sur la poignée intérieure aurait été impossible

Points particuliersPoints particuliersvisibles dans le PFFvisibles dans le PFF Et si la porte avait été maintenue en

position fermée en la bloquant sur un angle d ’ouverture nul? la serrure conducteur est bien décondamnée mais pas de décondamnation centralisée : la porte

n ’est pas détectée ouverte.

Modalités d ’applicationModalités d ’application

Difficultés : modéliser n ’est pas programmer « qu ’est ce qui garantit que le événements se

déclenchent ?» « comment modéliser un impulsion ? » « comment modéliser un processus continu ? »

Guide de modélisation image du « démon » animateur de modèles savoir ce que représentent les variables

Expertise de spécificationExpertise de spécification

B événementiel avec preuve

Travaux effectuésTravaux effectués

Modélisation B directe d ’une fonction train d ’atterrissage hélicoptère, telle que présentée sous forme d ’un schéma électronique Pour voir les précisions nécessaires à la modélisation Retraduction pour voir une modélisation B en format textuel

Recherche et modélisation d ’une spécification au dessus du schéma électrique Pour voir quelle serait une telle spécification Pour voir les résultats de preuve du schéma par rapport à

cette spécification

Modélisation directe : Modélisation directe : précisions nécessairesprécisions nécessaires Précisions sur la définition des états

électriques : 1 ou 0 suivant tension et résistance interne : norme ?

Précisions si perte alimentation carte : Temporisations remises à zéro quelle que soit la

durée de la coupure ? Sorties forcées à zéro dès alimentation insuffisante ?

Extrait modélisation Extrait modélisation retraduiteretraduiteLoi de rentrée :

Erre = Alim ET Cdre ET (Tvh/ OU Maintien force de rentrée)

C'est-à-dire : la sortie de pilotage de rentrée de train est active siet seulement si l'alimentation de la carte est active, que la commande de rentrée est active, et que :

- soit l'entrée train verrouillé haut est inactive ;- soit la carte est en phase de maintien force de rentrée

Recherche d ’une Recherche d ’une spécificationspécification Recherche a priori, a partir du schéma

électronique Premier niveau :

S ’il existe une volonté de rentrée de train, le train doit être rentré ou en train de rentrer.

S ’il existe une volonté de sortie de train, le train doit être sorti ou en train de sortir.

Recherche de spécificationRecherche de spécification

Deuxième niveau : une rentrée de train est en cours si la séquence

suivante est respectée : commande électrovanne de rentrée tant que les trois

retours « verrouillé haut » non présents maintien électrovanne de rentrée 2 secondes maintien alimentation hydraulique 2 secondes

Définition de la volonté : Rentrée si commande de rentrée et pas de commande

de sortie, et inversement nulle dans les autres cas

Montage B obtenuMontage B obtenu

Spécification1er niveau :

« si volonté... »

Spécification2ième niveau :

« rentrée si séquence ... »

modèle carte niveau schéma électronique

Questions pour la Questions pour la spécification :spécification :exemplesexemples Interruption séquence par coupure

alimentation carte ou changement rapide commande : la séquence doit-elle être recommencée ? les temporisations doivent-elles recommencer ?

Définition de la volonté : Quoi faire si les deux fils de commande (rentrée et

sortie) sont actifs ensemble ? Priorité à la sortie ?

Rôle de l ’électrovanne de dérivation ?

PreuvesPreuves

Spécification1er niveau :

« si volonté... »

Spécification2ième niveau :

« rentrée si séquence ... »

modèle carte niveau schéma électronique

cohérence interne : OK

n2 par rapport à n1 : OK

carte par rapport à n2 :

NON OK

Preuve non OK carte // Preuve non OK carte // spécificationspécification Spécification créée de toutes pièces ! exemple de preuves non OK :

Nous avons spécifié qu'en cas de disparition de la volonté (bouton en position intermédiaire), les deux électrovannes devaient être fermées.

Dans le cas de Cdre qui passe à 1 alors que Cdso est à 1, la spécification n'est pas respectée ; on a au moins Erre = 1 et peut-etre Erso = 1. Pourtant il n'y a plus de volonté affichée.

Conclusion généraleConclusion générale

Avantages de Avantages de l’approche Bl’approche B Le besoin est

mieux compris mieux exprimé

Sa formalisation est mieux tracée mieux maintenable

InconvénienInconvénientsts

Abstraire est difficile

Bien abstraire est très difficile Une bonne abstraction

paraît simple (simpliste)

Utilisation industrielle de BUtilisation industrielle de B

Dans un monde dominé par le court terme, y aura t-il beaucoup de systèmes entièrement prouvés ? Non !

Si la technique est éradiquée des circuits décisionnels, y aura t-il beaucoup de cahiers des charges prouvés ? Non !

Utilisation industrielle de BUtilisation industrielle de B

Savoir faire des modèles B ABSTRAITS, et néanmoins significatifs le raisonnement technique trop souvent une plongée

dans les détails

Promouvoir un raisonnement formel au plus haut niveau B système

Promouvoir des développements soignés conduisant à des systèmes sûrs Lutter contre la prolifération des systèmes pas sûrs