Méthodologie de développement de logiciels critiques

18h C dont contrôle / 2 crédits ECTS

Guy Vidal-Naquet & Joanna Tomasik (Gif)

Un logiciel est appelé critique quand une erreur lors de son exécution peut entrainer des conséquences graves, voire des pertes humaines. De nombreux exemples de telles erreurs existent malheureusement. Aussi le développement de ces logiciels doit être particulièrement rigoureux et se préter à une certification devant un organisme agréé. Un des critères qui doit être satisfait pour obtenir la certification est la réalisation, lors du développement, de preuve formelle de la correction du logiciel par rapport à ses spécifications.

Une méthode employée pour de nombreux projets importants est la « Méthode B » qui assure à chaque étape de l'écriture d'un logiciel, que les spécifications sont respectées. On évite d'avoir à prouver un logiciel après que celui-ci ait été réalisé, le logiciel obtenu étant garanti correct, dès la fin de sa réalisation. Il est intéressant de noter que les systèmes utilisant des logiciels développés avec cette méthode n'ont-jusqu'à présent- jamais eu d'erreur logicielle.

Nous présenterons cette méthode et l'outil logiciel associé. Un exemple de développement sera réalisé.

Cycle de développement, place des spécifications et des preuves.

Rappels sur la preuve des programmes par la méthode de Hoare.

Machines abstraites et spécifications.

Obligations de preuves

Raffinement et obligations de preuve associées.

Implémentation et obligations de preuve associées.

Présentation de l'outil associé «L'atelier B»

Réalisation de projet