Les logiciels temps réels peuvent être incorrects pour 3 raisons : non-respect du comportement fonctionnel du programme vis-à-vis de ses spécifications, non-respect des contraintes temporelles ou erreurs d'exécution. L'exposé traitera du troisième aspect qui inclut la détection d'overflows, d'exceptions arithmétiques (division par 0, racine carrée de nombre négatif...), de débordement de tableaux mais aussi des constructions indéterministes telles que variables non initialisées ou accès concurrents à une variable partagée.
Nous présenterons tout d'abord les principes de détection exhaustive des erreurs d'exécution d'un programme par analyse statique de code basée sur l'interprétation abstraite de programmes. Nous présenterons ensuite les résultats obtenus sur des logiciels ADA opérationnels de grandes tailles dans le domaine de l'espace et de l'avionique. Ces résultats ont été obtenus à l'aide de l'outil Polyspace Verifier dérivé du prototype IABC développé par Alain Deutsch alors chercheur à l'Inria.
En conclusion, nous présenterons les perspectives de développement de telles technologies.
| Page d'accueil Irisa | Séminaires
Irisa 1999 | Manifestations
scientifiques | Comment se rendre
à l'Irisa ? |
webmaster@irisa.fr, septembre 1999