Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Recomposition: A New Technique for Efficient Compositional Verification

Ian Dardik, April Porter, Eunsuk Kang

TL;DR

The paper tackles state-space explosion in compositional verification by making component selection a first-class problem and introducing recomposition, which builds new verification units $D_P, D_1,\dots,D_m$ from an initial decomposition $C_1,\dots,C_n$ via a surjective map $f$. It couples automated decomposition, static specification reduction, and a parallel portfolio of recomposition maps to drive efficient CRA-style verification, implemented in the Recomp-Verify tool for TLA$^+$ with a novel parallel composition operator. Empirically, recomposition achieves large state-space reductions and competitive or superior run times compared to TLC on distributed protocol benchmarks, and can handle certain infinite-state cases through static reduction. This work demonstrates that explicit, parallelized recomposition strategies can substantially improve scalable verification for complex concurrent systems.

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.

Recomposition: A New Technique for Efficient Compositional Verification

TL;DR

The paper tackles state-space explosion in compositional verification by making component selection a first-class problem and introducing recomposition, which builds new verification units from an initial decomposition via a surjective map . It couples automated decomposition, static specification reduction, and a parallel portfolio of recomposition maps to drive efficient CRA-style verification, implemented in the Recomp-Verify tool for TLA with a novel parallel composition operator. Empirically, recomposition achieves large state-space reductions and competitive or superior run times compared to TLC on distributed protocol benchmarks, and can handle certain infinite-state cases through static reduction. This work demonstrates that explicit, parallelized recomposition strategies can substantially improve scalable verification for complex concurrent systems.

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.
Paper Structure (4 sections, 1 figure)

This paper contains 4 sections, 1 figure.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. Protocol Description
  4. TLA+ Encoding

Figures (1)

  • Figure 1: Comparing traditional compositional verification against our recomposition method.