Back to University of Twente portal
| author: | Elwin Pater |
| title: | Partial Order Reduction for PINS |
| keywords: | model checking, state-space reduction, LTSmin |
| topics: | |
| committee: |
Michael Weber
, Jaco van de Pol , Dr. Dragan Bosnacki |
| started: | July 2010 |
| end: | May 2011 |
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
- A modular partial order reduction layer for an extension of PINS (i.e. language independent).
- Improvement on stubborn set algorithm.
- A modular LTL layer for PINS.
- Couvreur’s algorithm combined with General State Expanding Algorithms.
- A modular proviso implementation.