Vérification de propriétés invariantes par surapproximation

Florent Peres (1) , Pierre-Olivier Ribet (1) , François Vernadat (1) , Bernard Berthomieu (1)

1 LAAS - Laboratoire d'analyse et d'architecture des systèmes

Ce papier expose une technique d'abstraction des réseaux de Petri permettant de réduire l'explosion combinatoire lors de la validation de propriétés. L'abstraction proposée repose sur une fonction de renommage qui va permettre de cacher/confondre certaines places du réseau. Nous montrerons les résultats que nous avons obtenus ainsi que les limites de cette abstraction, nous soumettrons celle-ci à des exemples connus pour finalement apporter une comparaison avec des techniques existantes.

Mots clés: réseaux de Petri; abstraction; surapproximation; vérification

Domaines: Génie logiciel [cs.SE]

Florent Peres, Pierre-Olivier Ribet, François Vernadat, Bernard Berthomieu. Vérification de propriétés invariantes par surapproximation. Formalisation des activités concurrentes (2005), Mar 2005, Toulouse, France. ⟨hal-00422404⟩