99
Sécurité du système d’exploitation et des programmes
Chapitre 5
• la sémantique dénotationnelle se propose de créer le modèle sémantique d’un
système informatique en construisant des objets mathématiques qui expriment sa sémantique, ou en d’autres termes ce qu’il fait ;
• la sémantique axiomatique vise le même but en s’appuyant sur des formalismes empruntés à la logique ;
• la sémantique opérationnelle utilise aux mêmes fins les diagrammes d’état et
l’interprétation symbolique.
Entrer dans le détail de ces méthodes nous entraînerait au-delà du champ de cet
ouvrage, on pourra se reporter aux références indiquées par Wikipédia 5 .
Méthode B
Devant la difficulté de mise en œuvre des méthodes formelles évoquées à la section précédente, Jean-Raymond Abrial a choisi d’aborder ce problème par une
autre face : prouver la justesse et la sûreté du programme avant de l’écrire, et pour
cela il a créé la méthode B [7],[15] au milieu des années 1980. Elle a été utilisée dans
le cadre du projet de métro sans conducteur METEOR (Métro est-ouest rapide)
réalisé par Matra (maintenant Siemens Transportation System) pour le compte de la
Régie autonome des transports parisiens (RATP), pour construire de façon sûre
les parties du logiciel qui jouent un rôle critique pour la sécurité des passagers. La
partie du logiciel du métro METEOR réalisée grâce à l’Atelier B (l’outil informatique sous-jacent à la méthode [31] développé par la société ClearSy) comprend
près de 100 000 lignes de code Ada générées automatiquement. Notons qu’auparavant B Abrial avait créé le langage de spécification Z : peut-être un clin d’œil de
cinéphile aux amateurs des films de série B ou Z ?
Les premières démarches de preuve de programme tentaient d’appliquer des procédures de preuve à des programmes déjà construits. Il s’est assez vite révélé qu’un
programme final était un objet beaucoup trop complexe pour être soumis d’un
seul coup à une procédure de preuve, manuelle ou à plus forte raison automatique.
L’idée de B est donc d’élaborer la preuve en même temps que le programme. Le
langage de développement B permet de spécifier d’une part le programme proprement dit, d’autre part les propriétés dont on souhaite le voir doté.
5 http://en.wikipedia.org/wiki/Denotational_semantics
http://en.wikipedia.org/wiki/Hoare_logic
http://en.wikipedia.org/wiki/Operational_semantics
Sécurité du système d’exploitation et des programmes
Chapitre 5
• la sémantique dénotationnelle se propose de créer le modèle sémantique d’un
système informatique en construisant des objets mathématiques qui expriment sa sémantique, ou en d’autres termes ce qu’il fait ;
• la sémantique axiomatique vise le même but en s’appuyant sur des formalismes empruntés à la logique ;
• la sémantique opérationnelle utilise aux mêmes fins les diagrammes d’état et
l’interprétation symbolique.
Entrer dans le détail de ces méthodes nous entraînerait au-delà du champ de cet
ouvrage, on pourra se reporter aux références indiquées par Wikipédia 5 .
Méthode B
Devant la difficulté de mise en œuvre des méthodes formelles évoquées à la section précédente, Jean-Raymond Abrial a choisi d’aborder ce problème par une
autre face : prouver la justesse et la sûreté du programme avant de l’écrire, et pour
cela il a créé la méthode B [7],[15] au milieu des années 1980. Elle a été utilisée dans
le cadre du projet de métro sans conducteur METEOR (Métro est-ouest rapide)
réalisé par Matra (maintenant Siemens Transportation System) pour le compte de la
Régie autonome des transports parisiens (RATP), pour construire de façon sûre
les parties du logiciel qui jouent un rôle critique pour la sécurité des passagers. La
partie du logiciel du métro METEOR réalisée grâce à l’Atelier B (l’outil informatique sous-jacent à la méthode [31] développé par la société ClearSy) comprend
près de 100 000 lignes de code Ada générées automatiquement. Notons qu’auparavant B Abrial avait créé le langage de spécification Z : peut-être un clin d’œil de
cinéphile aux amateurs des films de série B ou Z ?
Les premières démarches de preuve de programme tentaient d’appliquer des procédures de preuve à des programmes déjà construits. Il s’est assez vite révélé qu’un
programme final était un objet beaucoup trop complexe pour être soumis d’un
seul coup à une procédure de preuve, manuelle ou à plus forte raison automatique.
L’idée de B est donc d’élaborer la preuve en même temps que le programme. Le
langage de développement B permet de spécifier d’une part le programme proprement dit, d’autre part les propriétés dont on souhaite le voir doté.
5 http://en.wikipedia.org/wiki/Denotational_semantics
http://en.wikipedia.org/wiki/Hoare_logic
http://en.wikipedia.org/wiki/Operational_semantics