Unfolding based verification of concurrent infinite-state systems

Nous proposons une technique de dépliage pour vérifier les systèmes concurrents infinis bien structurés. Certaines propriétés d'intérêt comme la bornitude, la couverture et la terminaison sont décidables grâce à la bonne structure de ces systèmes. D'autre part, le dépliage réduit efficacement l'explosion combinatoire en exploitant l'ordre partiel entre les événements des systèmes concurrents. Nous proposons une modélisation par structure d'événements pour des systèmes bien structurés élémentaires, tels les compteurs et les files de communication. Le dépliage d'un réseau de structures d'événements étant une structure d'événements, nous proposons ensuite une approche hiérarchique à la modélisation et à la vérification des systèmes, qui préserve la bonne structure. Enfin, nous proposons une technique d'élimination des événements redondants. La mise en œuvre de notre approche dans l'outil ESU nous permet de conclure à son efficacité.We propose an unfolding technique for verifying concurrent infinite-state systems that are well-structured. Some properties of interest such as boundedness, coverability and termination are decidable thanks to the well-structure of these systems. Moreover, the unfolding effectively reduces the combinatorial explosion by exploiting the partial order between events of concurrent systems. We propose a modelization using event structures for basic well-structured systems, such as counters and communication channels. As the unfolding of a synchronized product of event structures is an event structure, we obtain a hierarchical approach to modeling as well as to verifying systems, which preserves the well-structure. Finally, we propose a technique for eliminating redundant events. The implementation of our approach in the ESU tool allows us to conclude on its efficiency