Elwin Pater - Partial Order Reduction for PINS

author:Elwin Pater
title:Partial Order Reduction for PINS
keywords:model checking, state-space reduction, LTSmin
committee:dr.rer.nat. M. Weber (1st supervisor)
prof.dr. J.C. van de Pol
Dr. Dragan Bosnacki
graduation date:31 May 2011 (mark: 10/10)


Abstract

 

There are a lot of different tools used for formal verification of hard- and software. Both for the scientific purpose of comparing methods and tools, as well as the industrial use cases which may require combining various methods, a uniform interface for state space generation would improve the applicability of model checkers. One such interface is the partitioned next state interface (PINS) which is an abstraction layer between the model and the algorithms used for state space generation. In this thesis we develop a partial order algorithm that works using a minimal extension of the PINS interface, and is developed in a modular fashion.

Summary of contributions

  1. A modular partial order reduction layer for an extension of PINS (i.e. language independent).
  2. Improvement on stubborn set algorithm.
  3. A modular LTL layer for PINS.
  4. Couvreur’s algorithm combined with General State Expanding Algorithms.
  5. A modular proviso implementation.