Logiques temporelles basées sur actions pour la vérification des systèmes asynchrones

Overview & Synopsis

La vérification formelle est indispensable pour assurer la fiabilité des applications complexes et critiques comme les protocoles de télécommunication et les systèmes répartis. L'approche basée sur les modèles (model checking) consiste à traduire l'application vers un modèle système de transitions étiquetées, sur lequel les propriétés de bon fonctionnement, exprimées comme formules de logique temporelle, sont vérifiées au moyen d'algorithmes spécifiques. Ce rapport présente de manière unifiée les logiques temporelles basées sur actions qui sont actuellement les plus utilisées dans le contexte des systèmes parallèles asynchrones comportant du non-déterminisme. Les différentes logiques traitées (modales, arborescentes, régulières et de point fixe) sont illustrées à travers des exemples de propriétés typiques des systèmes parallèles asynchrones (sûreté, vivacité, équité) et sont comparées suivant l'expressivité, la facilité d'utilisation et l'efficacité des algorithmes de vérification associés.