CoInDiVinE: Parallel Distributed Model Checker for Component-Based Systems

TL;DR

CoInDiVinE is a parallel distributed model checker designed for hierarchical component-based systems, extending DiVinE with new input language and property logic, supporting partial order reduction and demonstrating good scalability.

Contribution

It introduces a new input language and property logic for model checking, along with a novel state space generation algorithm supporting partial order reduction.

Findings

Good scalability in parallel settings

Effective partial order reduction support

Extended framework with new language and logic

Abstract

CoInDiVinE is a tool for parallel distributed model checking of interactions among components in hierarchical component-based systems. The tool extends the DiVinE framework with a new input language (component-interaction automata) and a property specification logic (CI-LTL). As the language differs from the input language of DiVinE, our tool employs a new state space generation algorithm that also supports partial order reduction. Experiments indicate that the tool has good scaling properties when run in parallel setting.