|
|
Je suis actuellement doctorant au laboratoire CEDRIC du CNAM sous la direction de Jean-François Pradat-Peyre et Claude Kaiser.
Je fais partie de l'équipe Quasar composée de Sami Evangelista, Claude Kaiser, Jean-François Pradat-Peyre, Pierre Rousseau et Nicolas Trèves.
Je participe au développement de l'outil Helena, un vérifieur de modèles de réseaux de Petri colorés de haut-niveau et sa version parallèle à mémoire répartie Cyclades.
Recherche
Mon sujet de thèse porte sur la répartition et la parallélisation du processus de vérification de modèles.
Publications
-
Some Solutions to the Ignoring Problem
In Proceedings of 14th International SPIN Workshop on Model Checking Software, 2007.
[abstract] The ignoring problem refers to the fact that some actions may be infinitely postponed by a state space search algorithm that makes use of partial order reduction (POR). The prevention of this phenomenon is mandatory if one wants to verify more elaborate properties than the deadlock freeness, e.g., safety or liveness properties. We present in this work some solutions to this problem. In order to assess the quality of our propositions, we included them in our model checker Helena. We report the result of some experiments which show that our algorithms yield better reductions than state of the art algorithms like those implemented in the Spin tool.
-
Modelling remote concurrency with Ada. Case study of symmetric non-deterministic rendez-vous
In Proceedings 12th International Conference on Reliable Software Technologies, Ada-Europe, 2007.
[abstract] When developing concurrent software, a proper engineering practice is to choose a good level of abstraction for expressing concurrency control. Ideally, this level should provide platform-independent abstractions but, as the platform concurrency behaviour cannot be ignored, this abstraction level must also be able to cope with it and exhibit the influence of different possible behaviours. We state that the Ada language provides such a convenient abstraction level for concurrency description and evaluation, including distributed concurrency. For demonstrating it, we present two new cooperative algorithms based on remote procedure calls which, although simply stated, contain actual concurrency complexity and difficulties. They allow a distributed symmetric non-deterministic rendezvous. One relies on a common server and the second is fully distributed. Both realize a symmetric rendezvous using an asymmetric RPC modelled by Ada rendezvous. These case studies show that Ada concurrency features provide the adequate abstraction level both for describing and evaluating concurrency and for carrying out design decisions.
-
A simple positive flows computation algorithm for a large subclass of colored nets
In Proceedings 27th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'07), 2007.
[abstract] Positive flows provide very useful informations that can be used to perform efficient analysis of a model. Although algorithms computing (a generative family of) positive flows in ordinary Petri nets are well known, computing a generative family of positive flows in colored net remains an open problem. We propose in this paper a pragmatic approach that allows us to define an algorithm that computes a generative family of particular but useful positive flows in a large subclass of colored nets: the simple well-formed nets.
-
Distributed colored Petri net model-checking with Cycaldes
In Proceedings Parallel and Distributed Methods in verifiCation (PDMC) 2006, 2006.
[abstract] The major bottleneck of explicit model-checking tools is the limited amount of available memory. Distributed model-checking is an approach to tackle the combinatorial explosion problem. It consists in taking advantage of the aggregate of memory provided by a network of workstations to increase the amount of memory available for model-checking. Helena is the model-checker of the Quasar tool suite for concurrent software verification. It is a high-level colored Petri net explicit sequential model-checker that implements several state-space reduction and efficient state representation mechanisms. Helena is currently able to verify safety properties. In this paper we present Cyclades, a distributed version of Helena, that remains compatible with these reduction techniques. Several distribution mechanisms and some preliminary results are also provided.
-
Static Reductions for Promela Specifications
[.pdf]
Technical Report CEDRIC No 1005, 2006.
[abstract] The interleaving of concurrent processes actions leads to a combinatory explosion. There exists in Petri nets theory some structural reductions that combat the state explosion by agglomerating sequences of transitions into a single atomic transition. These reductions are easily checkable and preserve deadlocks, Petri nets liveness and any LTL formula that do not observe the modified transitions. Furthermore, they can be combined with others kinds of reductions such like partial-order techniques to obtain very effective reductions. We propose in this paper to adapt these reductions to Promela specifications by proposing some simple rules which give the possibility to automatically infer atomic steps in the Promela model while preserving the checked property. We demonstrate on typical example the efficiency of this approach and we propose some perspectives of this work.
-
Dynamic tasks verification with
Quasar
In Proceedings 10th International Conference on Reliable Software Technologies Ada-Europe 2005, 2005.Slides : [.pdf]
[abstract] The inclusion of dynamic tasks modelisation in Quasar, a tool for automatic analysis of concurrent programs, extends its applicative usefulness. However this extension leads to large size models whose processing has to face combinatory explosion of modelling states. This paper presents briefly Ada dynamic tasks semantic and dependences and then it explains the choice of an efficient generic modelling pattern. This implies to consider the naming, the hierarchy, the master retrieval, the termination of dynamic tasks and their synchronization dependences successively. The adequacy of both this modelling and the Quasar techniques is highlighted by the analysis of two non-trivial Ada programs. The large reduction factor between the initial and final state numbers of these program models shows that the state explosion can be limited, making automatic validation of dynamic concurrent programs feasible. -
Extending Quasar with dynamic tasks computation
[.pdf]
[.ps]
Rapport technique CEDRIC No 695, 2005.[abstract] The inclusion of dynamic tasks modelisation in Quasar, a tool for automatic analysis of concurrent programs, extends its applicative usefulness. However this extension leads to large size models whose processing has to face combinatory explosion of modeling states. This article is an extension of the paper "Dynamic tasks verification with QUASAR" accepted for publication in the 10th International Conference on Reliable Software Technologies Ada-Europe 2005. It gives some insight into the impact of the way used to name dynamic task in term of state space size by comparing different solutions on several examples.
Enseignements
Liens
 |
Le projet Quasar. |
 |
Les vérifieurs de modèle Helena et Cyclades. |
 |
Le groupe de recherche MeFoSyLoMa. |
 |
Le laboratoire Cedric. |
Contact
Adresse:
Christophe Pajault
292 rue Saint-Martin,
75141 Paris Cedex 03
France
Tel.:
+ 33 1 40 27 20 49
Email:
christophe -dot- pajault -at- cnam -dot- fr
last update : 23/07/07