Improved PROMELA BEEMing

title:Improved PROMELA BEEMing
keywords:compiler construction, PROMELA, model checking, BEEM
topics:Algorithms and Data Structures
contact:prof.dr. J.C. van de Pol & A.W. Laarman MSc
to be started:any time


Description

The goal of this project is to improve a large test suite of realistic case studies from the BEEM database for PROMELA, the input language of the SPIN model checker.

The BEEM database is a sizeable collection of verification case studies, e.g., communication and security protocols, models of synchronization primitives, and puzzles. Among other things, it is extremely useful as a real-life benchmarking set of model checking engines. It is cited is numerous scientific papers as the source of benchmarking models, and has established itself as a de-facto standard.

Models in the BEEM database are written in the DVE language, a syntax for extended finite state machines. Translators exist for several widely used tools and their specification languages, among them PROMELA.

Problem Statement

The translation for PROMELA is partly imprecise, which makes comparisons of SPIN runs with other tools unreliable. Moreover, even the correct translations are not using all of PROMELA's (and SPIN's) capabilities, thus needlessly pessimizing results for SPIN. For example, SPIN supports buffered communication channels, whereas the current translation to PROMELA always flattens buffered channels in to rendezvous channels and an accompanying array. This defeats SPIN's powerful partial-order reduction feature in many cases.

Tasks

  • Improve and implement the translator of DVE models from the BEEM database to PROMELA, so that the generated state spaces are provably identical. This requires extending an existing source-to-source compiler, or writing a new one.
  • Improve the translation by taking better advantage of SPIN's capabilities, e.g., by translating arrays guarded by rendezvous channels into buffered channels. This might require writing a static analyzer for either DVE or PROMELA.
  • Evaluate the achieved improvements on the BEEM database by comparing SPIN with native DVE state space generators.