Mardi 15 Janvier


Retour à la vue des calendrier
Mardi 15 Janvier
Heure: 12:15 - 13:30
Lieu: Salle A303, bâtiment A, Université de Villetaneuse
Résumé: Towards parallel verification of concurrent systems
Description: Hiba OUNI An efficient way to cope with the combinatorial explosion problem induced by the model checking process is to compute the Symbolic Observation Graph (SOG).
The SOG is defined as a condensed representation of the state space based on a symbolic encoding of the nodes (sets of states). It has the advantage to be much reduced comparing to the original state space graph while being equivalent with respect to linear time properties. Aiming to go further in the process of tackling the state space explosion problem, we propose to parallelize the construction of the SOG using three different approaches.
A multi-threaded approach based on a dynamic load balancing and a shared memory architecture, a distributed approach based on a distributed memory architecture and a hybrid (shared-distributed memory) approach that combines the two previous app roaches. We implement these algorithms, we study their performances and we compare them to each other and to the sequential construction of the SOG.
Experiments show that parallel approaches can improve drastically the performances of the SOG computation regarding a sequential construction.
Afterwards, we go a step forward in improving the SOG construction process by reducing, on the fly, the size of the graph. We provide a symbolic (LDD-based) dichotomy-based algorithm to canonically reduce the size of the SOG aggregates. We implement this algorithm within the three parallel approaches. We conduct experiments in order to measure the impact of the canonization on the SOG construction. Results show that the canonization allows to efficiently decrease memory consumption in all approaches. Also, it allows to improve the scalability for both distributed and hybrid approaches.