| Popis: |
Nous proposons de nouveaux algorithmes et de nouvelles structures de données pour la vérifi cation formelle de systèmes réactifs nis sur architectures parallèles. Ces travaux se basent sur les techniques de véri cation par model checking. Notre approche cible des architectures multi-processeurs et multi-coeurs, avec mémoire partagée, qui correspondent aux générations de serveurs les plus performants disponibles actuellement. Dans ce contexte, notre objectif principal est de proposer des approches qui soient à la fois effi caces au niveau des performances, mais aussi compatibles avec les politiques de partage dynamique du travail utilisées par les algorithmes de génération d'espaces d'états en parallèle ; ainsi, nous ne plaçons pas de contraintes sur la manière dont le travail ou les données sont partagés entre les processeurs. Parallèlement à la défi nition de nouveaux algorithmes de model checking pour machines multi-coeurs, nous nous intéressons également aux algorithmes de vérifi cation probabiliste. Par probabiliste, nous entendons des algorithmes de model checking qui ont une forte probabilité de visiter tous les états durant la vérifi cation d'un système. La véri fication probabiliste permet des gains importants au niveau de la mémoire utilisée, en échange d'une faible probabilité de ne pas être exhaustif ; il s'agit donc d'une stratégie permettant de répondre au problème de l'explosion combinatoire. |
