Abstract

Model checking is a model-based, automatic technique for the verification of finite state concurrent systems, which systematically checks all the reachable states of a model. An prominent example of model checking tool is SPIN.

This thesis introduces the systematic state exploration tool MAJoR, which explores all reachable states of a model and checks them for errors, similar to Spin. Unlike SPIN, MAJoR uses a virtual machine, implemented by an interpreter. The code of the high-level language is first translated to code of the intermediate language. This intermediate code is then executed using the interpreter. This thesis discusses the design and implementation of the virtual machine, the interpreter, the high-level language and the intermediate language.

SPIN uses Promela as its high-level source language. The source language designed for MAJoR is very close to Promela. Two additional features, not present in Promela, are added though: handshake communication with more than two processes, and pre- and post-conditions. Both are described in detail in this thesis.

Additional Resources

1. The paper