Symmetry reduction and symbolic data structures for model-checking of distributed systems
Institution:
Paris 6Disciplines:
Directors:
Abstract EN:
Les systèmes répartis deviennent omniprésents au quotidien, en particulier dans des domaines critiques, requérant une forte garantie de fiabilité. Les approches basées sur le test sont intrinsèquement non-exhaustives, rendant nécessaire l’usage de méthodes formelles. Parmi elles, nous nous concentrons sur le model-checking, qui explore tous les comportements d’un système pour s’assurer que sa spécification est respectée. Mais cette approche se heurte à l’explosion combinatoire : le nombre d’états d’un système réparticroît exponentiellement avec son nombre de composants. Nous retenons deux des nombreuses solutions à ce problème :- les symétries pour identifier des comportements similaires : ils partagent des propriétés communes, ce qui réduit le nombre d’états à explorer. - des structures de données compactes, comme les diagrammes de décision (DD), pour réduire l’empreinte mémoire de l’exploration. Nous proposons trois principales contributions :- La réduction par symétries et les DD sont théoriquement orthogonaux, mais se combinent mal en pratique, car l’efficacité des DD repose sur l’emploi d’algorithmes dédiés. Nous proposons un nouvel algorithme pour appliquer la réduction par symétries sur des DD, et démontrons son efficacité pratique. - Classiquement, les opérations sur les DD sont encodées après un pré-calcul de toutes les entrées possibles. Nous offrons un nouveau mécanisme de manipulation des DD, entièrement symbolique, qui évite un tel pré-calcul. Nous démontrons son efficacité pour encoder une relation de transition. - Nous montrons comment ces deux contributions peuvent être appliquées à un formalisme déjà existant, les Symmetric Nets with Bags.
Abstract FR:
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.