Évaluation de méthodes formelles de spécification

Abstract

Un des écueils pour l'acceptation des méthodes formelles dans l'industrie est l'absence d'un langage formel de spécification permettant d'exprimer et de vérifier de manière optimale tous les aspects d'un système informatique. En effet, différents langages sont proposés pour exprimer les spécifications relatives aux structures de données manipulées, au contrôle des différentes tâches à effectuer, aux contraintes temps réels, etc. Pour cela, l'emploi d'une méthode formelle inappropriée au domaine de l'application peut ajouter des difficultés notationnelles qui ne font souvent qu'obscurcir le problème. Il s'agit donc de choisir la méthode appropriée au domaine de l'application à développer, et aussi de choisir la manière de l'appliquer dans un cadre et une méthode de travail donnés. Une approche pour l'évaluation des méthodes formelles est proposée dans ce mémoire afin d'aider le développeur à choisir la méthode appropriée au domaine de l'application. Cette approche n'examine pas la qualité théorique de méthodes, mais plutôt leurs qualités pratiques concernant les notations et les outils, en les appliquant à un système de la facturation de commandes. Les deux étapes principales de cette approche sont (1) la définition d'une liste de critères pour l'évaluation de méthodes formelles; (2) l'évaluation de l'applicabilité des méthodes formelles au problème choisi, en se basant sur ces critères."--Résumé abrégé par UMI.