LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Tin tức » Nghiên cứu sinh

COLANGE Maximilien

Tiến sĩ
Nhóm nghiên cứu : MoVe
Ngày đi : 19-12-2013
Ban lãnh đạo nghiên cứu : Fabrice KORDON
Đồng hướng dẫn : 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.
Bảo vệ luận án : 10-12-2013 - 14h - Site Jussieu 25-26/105
Hội đồng giám khảo :
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)

Bài báo khoa học 2011-2018

 Mentions légales
Sơ đồ site |