Suivant Index

1   Introduction

1.1   Objectifs du cours

Les méthodes de modélisation (Fusion, UML) permettent d'analyser un cahier des charges pour identifier et concevoir les différents composants du logiciel à développer et préciser les comportements attendus.

Des notations (essentiellement des schémas) sont introduits pour faciliter une description non ambiguë du problème. Cependant ces méthodes restent informelles. Dans cette partie du cours, nous allons présenter une méthode rigoureuse de développement logiciel. Il s'agit d'introduire dans le procédé de modélisation: Le cours permettra également une initiation à la méthode B qui est utilisée dans certaines entreprises (Alsthom, Matra, Gemplus ...) pour la modélisation de logiciels critiques.

1.2   Contexte et motivations

1.2.1   Modélisation

Pour construire un logiciel, on démarre de spécifications générales informelles, nécessitant une modélisation de l'environnement dans lequel le logiciel sera utilisé. Cette modélisation est forcément approximative. Petit-à-petit le modèle est raffiné aussi bien dans la représentation des données que dans celle des opérations. On passe à un modèle mathématique qui permet le traitement rigoureux du problème.

1.2.2   Spécification formelle

C'est l'écriture de ce qui est attendu d'un programme dans un langage formel (analogue aux mathématiques) non ambiguë. Les spécifications formelles permettent de raisonner rigoureusement sur les propriétés attendues du programme (établir des invariants, montrer la complétude des spécifications ...)

1.2.3   Modèle d'un programme

Pour prouver qu'un programme réalise bien ce que l'on attend de lui, il faut avoir un modèle de l'exécution du programme.

Un modèle usuel d'un programme, est de le voir comme une fonction qui transforme la mémoire de la machine. Nous reviendrons plus en détail sur ce point.

Lorsque le programme et sa spécification sont exprimés dans un langage mathématique, on peut envisager de prouver qu'un programme exécute bien les tâches demandées.

1.2.4   Raffinement et réutilisation

Un programme exécute en général des tâches très complexes, le modèle est donc très gros, raisonner dessus est alors impraticable.

Mais il est également illusoire de penser écrire 100000 lignes d'assembleur sans erreur. Les programmes sont construits suivant deux principes : le raffinement et la réutilisation.

Définitions
Le raffinement est la décomposition d'un problème en sous-problèmes plus simples.

La réutilisation est la résolution d'un problème en utilisant des bibliothèques génériques dont les propriétés sont bien établies (efficacité, correction).

La preuve peut suivre le même cheminement, le raffinement correspond à une phase d'analyse, la réutilisation à une phase de synthèse où on cherche à appliquer des résultats connus (dont on n'est pas forcé de maîtriser la démonstration).

1.3   Applications

Le coût de développement d'une spécification formelle et de la preuve de correction d'un programme est très important. Ceci limite l'application de ces méthodes à des domaines particuliers où les besoins du zéro-défaut sont particulièrement importants.

Ce peut être pour diverses raisons : La présence de composants logiciels dans des fonctions de plus en plus critiques accroît de manière considérable le besoin de méthodes sûres et efficaces. D'autre part, le développement des logiciels est souvent confié à des organismes de sous-traitance, il faut être capable de vérifier leur qualité, de les intégrer, de les adapter.

1.3.1   Comment s'assurer qu'un programme critique est correct

Certification
Les programmes critiques ne peuvent être mis en service qu'après avoir fait l'objet d'une certification par des instances compétentes. Pour l'instant les critères de certification reposent essentiellement sur le test, et les labels qualité du procédé de développement des entreprises. La certification se fait souvent sur des critères d'appréciation plus subjectifs que scientifiques. Cependant, depuis quelques années, des normes sont apparues dans le domaine de la sécurité des informations (critères communs) qui exigent des modélisations formelles et des preuves de correction, pour les normes les plus exigeantes.

Tests
Le test est un élément important de la validation d'un programme. On peut espérer que des programmes très largement utilisés contiendront moins de défaut que des programmes peu utilisés. Cependant ce n'est vrai que pour des programmes qui évoluent peu : on peut comparer par exemple un traitement de texte commercial dans lequel de nouvelles fonctionnalités (et de nouveaux bugs) sont constamment introduits et un compilateur d'un langage stable. Il n'est pas toujours pertinent de déployer un programme avant d'être sûr de son fonctionnement (penser à Ariane, ou aux cartes bancaires). Tester de manière efficace (en temps, en couverture) un programme est très difficile. Lorsqu'une modification est apportée à un programme, celle-ci peut avoir des répercussions dans d'autres parties du programme, en conséquence les tests doivent souvent être repris à zéro.

Les tests sont indispensables, mais ils ne garantissent pas en général une correction totale et ont également un coût très élevé.

Ce qu'il faut retenir

1.3.2   Langage de spécification

Lorsqu'on modélise un problème, il faut choisir le langage dans lequel seront écrites les spécifications. En Angleterre, s'est développée une méthode appelée Z qui repose sur la théorie des ensembles [6]. L'idée est que les modélisations de systèmes d'information nécessitent de décrire des ensembles, des fonctions et des relations entre ces ensembles. Cette méthode reste très abstraite et n'est pas directement supportée par des outils de programmation ou de preuve. Cependant elle a beaucoup influencé le développement de la méthode B.

1.3.3   Qu'est-ce que B ?

La méthode B a été inventée par Jean-Raymond Abrial au milieu des années 80. Jean-Raymond Abrial était alors consultant auprès de la RATP. On lui a demandé d'évaluer la sécurité des programmes de freinage pour le RER A (la distance entre les rames devait être réduite ce qui rendait critique cette partie du code). Il a rendu un avis négatif sur le code ce qui a entraîné un retard important dans la mise en service.

Son idée a donc été de proposer une méthode à la fois rigoureuse et effectivement utilisable en milieu industriel. La méthode développée se devait de rester proche des habitudes des programmeurs, et être intégrée à un environnement de preuve.

La RATP a beaucoup soutenu le développement des méthodes formelles (en imposant leur utilisation à ses sous-traitants) et en particulier de la méthode B. La partie critique du métro Meteor en particulier a été développée ainsi.

Les grands principes de la méthode B sont : Une machine abstraite se présente comme un objet avec des variables représentant l'état de la machine et des opérations décrites par leur propriétés. Par ces aspects, la méthode B se rapproche des méthodes de modélisation objet. C'est cette notion de machine abstraite et les procédés de raffinement et d'implantation qui lui sont associés qui constitue la partie la plus intéressante de la méthode B.

La phase d'implantation permet d'établir une chaîne sûre entre des spécifications de haut niveau et un code exécutable qui peut être engendré automatiquement.

1.3.4   Outils

Un grand intérêt de la méthode B est d'être supportée par des outils. Il existe essentiellement deux systèmes développés par des sociétés commerciales sous l'impulsion (passée ou présente) de J.-R. Abrial. L'un est B-tool développé en Angleterre par la société B-core [3]. L'autre est l'atelier B [2] développé en France par la société ClearSy (anciennement Steria) .

Ce qu'il faut retenir

1.4   Plan du cours

  1. Bases du langage
  2. Machines abstraites
  3. Raffinement
  4. Implémentation
  5. Application
Suivant Index