Formal Validation with Model-Checking Techniques
Résumé
"Un défi bien connu dans le domaine des méthodes formelles est
d'améliorer leur intégration dans les processus de développement
logiciel. Si nous voulons que ces techniques soient utilisables à terme
dans le contexte de développement de logiciels industriels et de taille
significatives, cela nécessite encore d'investir des travaux de
recherche tant sur le plan technique que méthodologique.
D'une part, une meilleure gestion de la complexité des modèles à simuler
doit être atteinte au regard de la performance des calculateurs
actuels. D'autre part, les méthodologies d'emploi sont à définir et à
adapter aux processus déjà mis en place par les ingénieurs dans les
unités de production.
Nous rendons compte, dans cette présentation, de travaux de recherche
menés dans le domaine particulier des systèmes embarqués. Ceux-ci ont
abordé des points durs scientifiques impliquant des aspects techniques
pouvant contribuer au
"passage à l'échelle" en cherchant, par exemple, à réduire l'espace des
états parcourus lors des simulations nécessaires pour la vérification de
propriétés.
Nous avons proposé, pour cela, une technique basée sur la notion de
contexte spécifié dans un langage ad-hoc nommée CDL (Context Description
Language). Nous avons également proposé des éléments méthodologiques
permettant un meilleur ancrage dans les processus de développement
existants. Ils concernent l'identification, la structuration et la
formalisation des données nécessaires aux activités de vérification
comme la spécification formelle des contextes de réduction, des
propriétés formelles et les modèles applicatifs à simuler.
Dans ce contexte, nous avons proposé un outil d'analyse nommé OBP
(Observer-Based Prover) qui nous a permis de mener de nombreuses
expérimentations sur des applications fournies par des industriels du
domaine aéronautique, automobile et des systèmes électroniques. A partir
des résultats obtenus, nous traçons un ensemble de perspectives pour le
développement de recherches futures.