Symmetry Reduction and Symbolic Data Structures for Model-Checking of Distributed Systems.
Distributed systems are becoming omnipresent in our daily life, especially in critical domains, thus requiring a strong guarantee of reliability.
Approaches like testing are inherently not exhaustive, so that formal methods are needed.
Among those, we focus on model-checking, that consists in exploring exhaustively all the behaviors of a system to ensure that the specification is enforced. However, this approach faces the “combinatorial explosion” problem: the number behaviors of a distributed system increases exponentially with its number of components.
To tackle this explosion, several approaches have been proposed.
We focus on two of them:
- symmetries to identify similar behaviors: they share similar properties, thus allowing to reduce the number of behaviors to explore;
- symbolic compact data structures, namely decision diagrams (DD), to reduce the memory footprint of the explored behaviors. We propose three main contributions:
- Symmetry reduction and DD are theoretically orthogonal techniques, but are not known to combine well in practice, because efficiency of DD heavily relies on the use of dedicated algorithms.
We propose a novel algorithm to use symmetry reduction on DD, and demonstrate experimentally its efficiency.
- Classical operations on DD are encoded using a pre-computation of all possible inputs.
We offer a new mechanism of manipulation of DD, fully symbolic, that avoids such a pre-computation.
We demonstrate its efficiency to encode a transition relation, and to improve our symmetry reduction algorithm.
- We show how to use the two previous contributions to model-check an existing class of models, the Symmetric Nets with Bags.
Defence : 12/10/2013 - 14h - Site Jussieu 25-26/105 Jury members : Pr. Ahmed Bouajjani [rapporteur] (Université Paris Diderot)
Pr. François Vernadat [rapporteur] (INSA Toulouse)
Dr. Souheib Baarir (Université Paris Ouest Nanterre la Défense)
Pr. Béatrice Bérard (Université Pierre et Marie Curie)
Pr.Dr.-Ing. Monika Heiner (Brandenburg University of Technology Cottbus)
Dr. Tommi Junttila (Aalto University)
Pr. Fabrice Kordon (Université Pierre et Marie Curie)
Dr. Yann Thierry-Mieg (Université Pierre et Marie Curie)
H. Metin, S. Baarir, M. Colange, F. Kordon : “CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving”, Tools and Algorithms for the Construction and Analysis of Systems -- TACAS, Tools and Algorithms for the Construction and Analysis of Systems 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proce, Tessaloniki, Greece (2018)
F. Kordon, A. Linard, D. Buchs, M. Colange, S. Evangelista, K. Lampka, N. Lohmann, E. Paviot‑Adet, Y. Thierry‑Mieg, H. Wimmel : “Report on the Model Checking Contest at Petri Nets 2011”, LNCS Transactions on Petri Nets and Other Models of Concurrency, vol. 7400 (VI), Lecture Notes in Computer Science, pp. 169-196, (Springer Verlag), (ISBN: 1867-7193) (2012)
M. Colange, F. Kordon, Y. Thierry‑Mieg, S. Baarir : “State Space Analysis using Symmetries on Decision Diagrams”, Application of Concurrency to System Design 12th International Conference on Application of Concurrency to System Design (ACSD'2012), Hamburg, Germany, pp. 164-172, (IEEE Computer Society) (2012)