Abstract FR:

Une propriete de surete sur un systeme est verifiee par tous ses etats accessibles. Ces proprietes sont generalement difficiles a etablir, meme pour des systemes sequentiels. Cette these se place dans le cadre de la verification et du calcul de telles proprietes pour des systemes paralleles modelises a l'aide de reseaux de petri. Les proprietes sont exprimees sous la forme de disjonctions d'inequations lineaires sur le marquage des places. La methode de verification proposee dans ce memoire est basee sur la transformation d'assertions et sur l'exploitation de la structure des reseaux de petri. La verification est realisee en un nombre fini d'etapes pour les systemes bornes et pour une classe particuliere de proprietes generalisant les verrous pour les reseaux non-bornes. Cette methode de verification permet l'elaboration d'une methode de calcul. Ces deux methodes sont definies de facon generique sur les systemes de transitions, puis appliquees aux reseaux de petri. La methode de verification est aussi specialisee pour des extensions des reseaux de petri (arcs inhibiteurs, reseaux a priorites, transitions gardees, les reseaux automodifiants). La methode de verification a aussi ete etendue de facon a traiter des proprietes exprimant le marquage ou le non-marquage des places. Il s'agit donc de proprietes etendant les verrous et les trappes. Un nouvel algorithme de calcul est defini pour ces proprietes. Cet algorithme a donne lieu a une implementation. Une analyse purement structurelle de ces proprietes est detaillee dans le dernier chapitre de ce memoire