An Architecture for Verification with Extended Labeled Transition Systems

Abstract

This thesis lays out a common architecture for a software system meant for verification of correctness of concurrent state machines. The purpose of the architecture is to enable implementation and combination of different reductions and other manipulations, that give perspectives into the behaviour of the system.

The LTS model and associated techniques are presented for a mathematical basis for the system. The system is made flexible using extensive modularization. Even techniques traditionally contained inside the parallel composer, such as cut states and stubborn sets are extracted into modules. Techniques are presented to avoid the performance loss of modularization using compile time processing.