PROMELA library

The PROMELA library is an OCaml library providing types and functions to create, analyze and modify PROMELA programs as used by the Spin model checker. The library provides types for PROMELA expression, statements, processes and models to create PROMELA programs as OCaml data structures. It includes functions to analyze the programs and also to generate valid PROMELA text-representation of the data structures.

As a demo of how to write code generators and also as synthetic benchmark for your tools there is the Dining Philosophers Problem (dpp) generator. This tool creates a model of n philosophers trying to obtain two shared forks at once.

To finally create a PROMELA text representation from a binary model you can use the spinmodel tool.

  1. Install Spin, OCaml, findlib and extlib
  2. Download and extract libpromela; then do a make all and make install in the extracted directory
  3. Download anf extract dppgenerator and spinmodel; do a make all and make install in the extracted directories
  4. Create a model with 2 philosophers: dppgenerator -p2 -ophilosophers.pmo
  5. Convert the binary model to a text file: spinmodel philosophers.pmo
  6. Find the race condition with spin: spin -a; cc pan.c -opan; ./pan

The source code has been written at the chair of robotics and embedded systems at Technische Universität München by Markus Weissmann and Florian Pichlmeier.

The releases of the PROMELA library and tools can be downloaded from OCamlForge. The API of the PROMELA library is also available online. The source code is released as open source under the (new) BSD license.

This document was translated from LATEX by HEVEA.