Team : MoVe
Departure date : 12/19/2013
Supervision : Fabrice KORDON
Co-supervision : BAARIR Souheib, THIERRY-MIEG Yann
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 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, Proceedings,, Tessaloniki, Greece (2018)
- A. Linard, B. Barbot, D. Buchs, M. Colange, C. Démoulins, L. Hillah, A. Martin : “Layered Data: A Modular Formal Definition without Formalisms”, CEUR-WS.org, vol. 1591, CEUR Workshops Proceedings, Toruń, Poland, pp. 287-306 (2016)
- M. Colange : “Symmetry Reduction and Symbolic Data Structures for Model-Checking of Distributed Systems.”, thesis, defence 12/10/2013, supervision Kordon, Fabrice, co-supervision : Baarir, Souheib, Thierry-mieg, Yann (2013)
- M. Colange, S. Baarir, F. Kordon, Y. Thierry‑Mieg : “Towards Distributed Software Model-Checking using Decision Diagrams”, 25th International Conference on Computer Aided Verification (CAV), vol. 8044, Lecture Notes in Computer Science, Saint-Petersbourg, Russian Federation, pp. 830-845, (Springer Verlag) (2013)
- M. Colange, F. Kordon, Y. Thierry‑Mieg, S. Baarir : “State Space Analysis using Symmetries on Decision Diagrams”, 12th International Conference on Application of Concurrency to System Design (ACSD'2012), Hamburg, Germany, pp. 164-172, (IEEE Computer Society) (2012)
- M. Colange, L. Hillah, F. Kordon, P. Parutto : “Extreme Symmetries in Complex Distributed Systems: the Bag-Oriented Approach”, Development, Operation and Management of Large-Scale Complex IT Systems, 17th Monterey Workshop, Revised Selected Papers, vol. 7539, Lecture Notes in Computer Science, Oxford, United Kingdom, pp. 330-352, (Springer) (2012)
- 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) (2012)
- M. Colange, S. Baarir, F. Kordon, Y. Thierry‑Mieg : “Crocodile: a Symbolic/Symbolic tool for the analysis of Symmetric Nets with Bag”, 32nd International Conference on Petri Nets and Other Models of Concurrency (ICATPN 2011), vol. 6709, Lecture Notes in Computer Science, Newcastle, United Kingdom, pp. 338-347, (Springer) (2011)