Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Thèse:   
Vers la vérification de propriétés de sûreté pour des systèmes infinis communicants: décidabilité & raffinement des abstractions

Date 2011-06-27  14:00-16:00
TitreVers la vérification de propriétés de sûreté pour des systèmes infinis communicants: décidabilité & raffinement des abstractions 
RésuméCette thèse propose des points d'attaque à la question de l'atteignabilité des états de contrôle pour des logiciels distribués basés sur des canaux fifo non bornés et fiables qui est indécidable dans le cadre général : primo, une sur-aproximation basé sur l'approche abstraire-tester-raffiner qui mène à un semi-algorithme type CEGAR et qui est implémenté dans l'outil McScM; secundo, une restriction au modèle de base qui d'une part est important en pratique, et qui d'autre part permet de résoudre la question l'atteignabilité dans 2ExpTime-complet; et, tertio, des premiers pas à une procédure de model checking MSO basée sur des ordres partiels, inspiré par des grammaires de graphe. En résumant, les résultats présentés généralisent les résultats connus et élargissent la (semi-)décidabilité de la vérification automatique de sûreté aux nouvelles classes des systèmes infinis communicants.  
LieuAmphi 
LaboratoireLaBRI 
DoctorantAlexander Heußner 
Directeur de thèseAnca Muscholl 



Aucun document lié à cet événement.

Retour
Retour à l'index