Formal Validation with Model-Checking Techniques

International audience"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