Validating Promela Models with the ProB Model Checker
Author
Dennis Winter
Abstract
Model checking is a technique applied for formal verification of software systems. Specifications, written in Promela (Process Meta-Language) can be validated by the SPIN (Simple Promela Interpreter) model checker. ProB is a platform which includes an animator and a model checker for the B-Method. We present the implementation of a Promela plugin, which allows ProB to animate and validate Promela models. The plugin consists of two main components, a compiler which compiles Promela code into a self-defined Prolog syntax, and an interpreter written in Prolog.
We describe how to develop the compiler using the parser generator SableCC and give a detailed description of the Promela interpreter, which interacts with the ProB model checker to construct the state graph. Utilizing pre-existing ProB features, we were able to perform guided animation on Promela models with state properties visible at any time and concurrent highlighting of the underlying source code.
By extending the ProB LTL (Linear Temporal Logic) model checker we were able to validate ProB models with respect to a given LTL formula. We demonstrate a technique to verify our interpreter with the concept of Never Claims used by the SPIN model checker. While the scalability of our interpreter is still inferior to SPIN, it can be further improved by model checking optimization techniques, which we also present in this master thesis.
Advised By
Download: PDF