LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Tin tức » Nghiên cứu sinh

DURET-LUTZ Alexandre

Tiến sĩ
Nhóm nghiên cứu : MoVe
Ngày đi : 11-07-2007
https://www.lrde.epita.fr/~adl/
Ban lãnh đạo nghiên cứu : Fabrice KORDON
Đồng hướng dẫn : POITRENAUD Denis

Contributions à l'approche automate pour la vérification de propriétés de systèmes concurrents

L'approche automate pour le model checking de propriétés temporelles à temps linéaire est une technique classique de vérification formelle de systèmes concurrents. Un système, ainsi qu'une propriété qu'on souhaite y vérifier, sont modélisés sous forme d'automates reconnaissant des mots infinis (des ?-automates). Des manipulations de ces automates permettent d'établir si le système vérifie la propriété ou non. Dans cette thèse nous nous focalisons sur un type particulier d'?-automates : les automates de Büchi généralisés basés sur les transitions (TGBA). Dans un premier temps nous revisitons les deux principales étapes de l'approche : la traduction de formules de logique temporelle à temps linéaire en TGBA et le test de vacuité (emptiness check) d'un TGBA. Pour chacune, nous proposons des améliorations des algorithmes existants, et comparons ces algorithmes pour montrer l'intérêt des TGBA. Dans un deuxième temps, nous proposons deux variations du test de vacuité. L'une peut être utilisée avec certains algorithmes qui réduisent l'automate représentant le système en regroupant ses états de façon symbolique. Elle utilise des tests d'inclusion entre ces regroupements d'états pour guider la construction à la volée de l'automate. L'autre est une généralisation aux automates de Streett (à nouveau basés sur les transitions); elle permet de prendre en compte des hypothèses d'équité forte lors de la vérification.
Bảo vệ luận án : 10-07-2007 - 14h30 - Site Passy-Kennedy - salle 549
Hội đồng giám khảo :
M. Ahmed Bouajjani, Professeur à l'Université Paris 7 [Rapporteur]
M. François Vernadat, Professeur à l'INSA de Toulouse [Rapporteur]
M. Jean-Michel Couvreur, Professeur à l'Université d'Orléans
M. Claude Girault, Professeur émérite à l'Université Paris 6
M. Alain Griffault, Maître de conférences à l'Université Bordeaux 1
M. Serge Haddad, Professeur à l'Université Paris-Dauphine
M. Fabrice Kordon, Professeur à l'Université Paris 6
M. Denis Poitrenaud, Maître de conférences à l'Université Paris 5

2 Tiến sĩ 2014

Bài báo khoa học 2004-2017

 Mentions légales
Sơ đồ site |