Retour au site du LAAS-CNRS

Résumé

La première partie de ce document présente le formalisme VAL développé pour la modélisation (conception et vérification) de systèmes dynamiques de communication. Pour ces systèmes le nombre et/ou le type d'agents, ainsi que leur organisation, évoluent dynamiquement. Les agents, structurés en classes, sont les éléments actifs du système: ils communiquent avec les autres (de façon synchrone ou asynchrone), ils peuvent disparaître et/ou créer d'autres agents. Le comportement d'une classe d'agents est décrit dans une extension des réseaux de Petri Prédicat-Transition. Les extensions proposées dans VAL concernent les aspects liés à la communication et au dynamisme. La seconde partie de cet exposé concerne la vérification et focalise sur le problème de l'explosion combinatoire. Une approche commune à la vérification de systèmes concurrents consiste à construire au préalable l'espace des états accessibles du système et à l'analyser par des techniques de model-checking. Un inconvénient majeur réside dans l'explosion combinatoire qui limite dans la pratique l'utilisation de ces techniques. Pour réduire cette explosion, nos travaux ont suivi les techniques dites "ordre partiel" qui permettent de réduire la part d'explosion relative à la représentation du parallélisme par l'entrelacement d'actions. Nous introduisons les graphes des pas couvrants comme alternative aux systèmes de transitions. Dans un GPC des pas de transitions indépendantes sont substitués autant que possible à l'hypercube qui aurait résulté de l'exploration séquentielle entrelacée de ces transitions. Le bénéfice potentiel réalisé par ce type de substitution est localement exponentiel en le nombre de transitions fusionnées. Différents algorithmes de "construction à la volée" de graphes couvrants ont été proposés pour permettre la vérification de propriétés d'accessibilité générales (absence de blocage, vivacité) ou spécifiques (bisimulation, sémantiques de refus).

Abstract

This thesis presents our contributions in the domain of the modeling and the verification of communicating systems. The first part of this thesis presents VAL formalism dedicated for the modeling and the verification of dynamic communicating systems. For such systems, the agent number and their kind dynamically evolve. Agents structured in classes constitute the reactive part of the system, they communicate in a synchronous or asynchronous way. Agents may disappear and/or create new instances. Agent behavior is described by an extension of predicate/transition nets. Extensions furnished in VAL concern communication and dynamism. The second part of this thesis concerns verification and focuses on combinational explosion problem. A common approach to the formal verification needs as a preliminary step the exhaustive exploration of the state space, then an analysis is performed using standard model checking techniques. The combinational explosion is the main limitation of this approach. To reduce this explosion, our work uses partial order techniques which are efficient for reducing the state explosion due to the representation of parallelism by interleaving. We introduce the notion of "covering step graphs" (CSG) as an alternative to labeled transition systems. In a CSG, steps of independent transitions are substituted as much as possible to the hypercube which would result from the firing of the independent transitions. The potential benefit of such a substitution may be exponential with respect to the number of "merged" independent transitions. Different algorithms for the "on the fly" derivation of CSG derivation are proposed in order to preserve general reachability properties (presence of deadlock, liveness) or specific one such as weak bisimulation and failure semantics.

Mots-Clés / Keywords

Systèmes concurrents; Verification; Réseaux de Petri; Explosion combinatoire; Ordres partiels; Concurrent systems; Petri nets; Combinational explosion; Partial order;