Matière "NIE18 - VAS : Vérification par analyse statique"

1 - Fiche descriptive

Langue

Cette matière est enseignée en français.

Objectifs

L’importance et la complexité du logiciel dans les systèmes critiques augmentent régulièrement ainsi que les contraintes de sûreté et de fiabilité imposées par les autorités de certification. Il dévient alors de plus en plus difficile de vérifier la correction de ces systèmes en s’appuyant exclusivement sur des techniques de tests et sur le respect d’un processus de développement éprouvé. Il devient nécessaire de s’appuyer sur des techniques formelles pour prouver mathématiquement leur correction. Pour donner de bons résultats et passer à l’échelle de systèmes industriels réels, celles-ci doivent être adaptées au type de systèmes et de propriétés considérées.
Les nouvelles chaînes de développement de logiciel pour les systèmes critiques en cours de déploiement s’appuient sur des combinaisons de langages de modélisation/programmation et de techniques de vérification pour répondre aux différents objectifs de certification.

Programme/Contenu

Cet enseignement présente ce contexte ainsi que trois des techniques de vérification formelle les plus utilisées pour la construction de ces chaînes. Il s’agit de techniques exhaustives, qui ne demandent pas d’exécution du système final, et reposent sur différentes abstractions de ce système : les méthodes déductives, la vérification de modèle et l’interprétation abstraite.
La première consiste à prouver mathématiquement de manière semi-automatique que le système respecte sa spécification.
La deuxième consiste à faire un test exhaustif de l’ensemble des propriétés de la spécification sur tous les états possibles d’une, ou plusieurs, abstractions adéquates du système.
La troisième consiste à effectuer une exécution abstraite du système pour parcourir l’ensemble des chemins d’exécution possibles et déterminer les propriétés les plus fortes que le système possède. Cette technique donnera lieu aux travaux pratiques et bureau d’étude.
Ces techniques ont été mise en œuvre dans les chaînes de développement de systèmes réels tels le métro METEOR ou les commandes de vol électrique de l’A380 et sont en cours de généralisation sur les systèmes futurs.

Mots clés

  • Analyses statiques, Vérification des systèmes

2 - Organisation de la matière

UE utilisant cette matière

UE Promotions
NIE - LOG : Parcours Logiciel Ingénieur ENSEEIHT Informatique 3ème année

Volume horaire

Element Volume horaire
Colloque 0.0
Cours magistral 15.75
Travaux pratiques 5.25
Bureau d'études 0.0
Total 21.0

Examens

Type Forme Coefficient
Contrôle continu Ecrit 0.0

3 - Contacts

Responsables

  • Pantel Marc

Enseignants

  • Pantel Marc
  • Thirioux Xavier