Recomposition: A New Technique for Efficient Compositional Verification

TL;DR

This paper introduces a novel compositional verification framework that improves efficiency by explicitly selecting and recomposing system components, utilizing heuristics and parallelization, demonstrated on TLA+ distributed protocols.

Contribution

The paper presents a new framework for component selection in compositional verification, including heuristics for recomposition map search and parallel execution, implemented in a TLA+ model checker.

Findings

Achieves competitive performance with TLC on distributed protocol benchmarks.

Introduces heuristics for efficient recomposition map selection.

Demonstrates effectiveness of recomposition in model checking.

Abstract

Compositional verification algorithms are well-studied in the context of model checking. Properly selecting components for verification is important for efficiency, yet has received comparatively less attention. In this paper, we address this gap with a novel compositional verification framework that focuses on component selection as an explicit, first-class concept. The framework decomposes a system into components, which we then recompose into new components for efficient verification. At the heart of our technique is the recomposition map that determines how recomposition is performed; the component selection problem thus reduces to finding a good recomposition map. However, the space of possible recomposition maps can be large. We therefore propose heuristics to find a small portfolio of recomposition maps, which we then run in parallel. We implemented our techniques in a model checker for the TLA+ language. In our experiments, we show that our tool achieves competitive performance with TLC-a well-known model checker for TLA+-on a benchmark suite of distributed protocols.