Key points are not available for this paper at this time.
La vérification de programmes est une approche prometteuse pour améliorer la qualité des programmes, car elle peut rechercher toutes les exécutions possibles d'un programme pour des erreurs spécifiques. Cependant, la nécessité de décrire formellement le comportement correct ou les erreurs constitue un obstacle majeur à l'adoption généralisée de la vérification de programmes, puisque les programmeurs ont historiquement été réticents à écrire des spécifications formelles. Automatiser le processus de formulation des spécifications éliminerait cet obstacle à la vérification des programmes et en améliorerait la praticité. Cet article décrit l'extraction de spécifications, une approche d'apprentissage automatique pour découvrir les spécifications formelles des protocoles que le code doit respecter lorsqu'il interagit avec une interface de programme d'application ou un type de données abstrait. Partant de l'hypothèse qu'un programme fonctionnel est suffisamment débogué pour révéler de fortes indications de protocoles corrects, notre outil infère une spécification en observant l'exécution du programme et en résumant de manière concise les motifs d'interaction fréquents sous forme de machines d'état qui capturent à la fois les dépendances temporelles et de données. Ces machines d'état peuvent être examinées par un programmeur, pour affiner la spécification et identifier les erreurs, et peuvent être utilisées par des outils de vérification automatique pour trouver des bogues. Notre expérience préliminaire avec l'outil d'extraction a été prometteuse. Nous avons pu apprendre des spécifications qui capturaient non seulement le protocole correct, mais découvraient également des bogues graves.
Ammons et al. (Mar,) ont étudié cette question.