Back to University of Twente portal
| author: | Riemer van Rozen |
| title: | A Debugging Framework for NIPS |
| keywords: | NIPS, debugging, model checking |
| topics: | |
| committee: |
Theo Ruys
, Michael Weber , Arend Rensink |
| end: | October 2007 |
Abstract
The NIPS VM is a non-deterministic virtual machine to be used for state space generation in model checkers. The NIPS VM typically plays the role of the state space generation back-end in an explicit state model checking framework. Using the NIPS VM as tool back-end saves the tool engineer the often complex and time-consuming task of having to design and implement a model checking engine. Furthermore, the design allows the reuse of modeling languages and common (byte code) analyses. However, working with the NIPS VM poses some problems:
- State vectors within the NIPS VM are opaque binary objects.
- Consequently, the NIPS VM misses debugging functionality.
- Although the NIPS VM is designed to be an embeddable component for state space generation, it is unclear how it can actually be embedded.
The goal of this research is to further ease the use of the NIPS VM as a reusable component for state space generation that is part of a extensible tool set of explicit state model checker components.
In order to achieve this we have developed a language with a simple multi-use readable format for Static Debugging Information (SDI) and the SDI Framework for state manipulation, which is based on this language. The framework can generally be applied to debugging designs for explicit state model checkers using state vectors. It is used in particular for a debugger for the NIPS VM. The SDI framework solves the following problems regarding debugging functionality and state introspection. It provides debugging API, a means for programs e.g. debuggers, to perform meta-level operations at run-time.
In order to support the NIPS Debugger we add a debugging API to the NIPS VM based on the SDI Framework. We extended the NIPS VM Tool Set with a debugger that allows users to simulate the behaviour of NIPS byte code. The debugger graphically depict states and transitions at source-level. In an interactive simulation, which may be guided by a counter-example, users may choose transitions and edit state values. The NIPS Debugger and the SDI Framework are evaluated in a case study of the debugger in comparison with SPIN.