Skip to content

Latest commit

 

History

History
105 lines (79 loc) · 2.91 KB

README.rst

File metadata and controls

105 lines (79 loc) · 2.91 KB
Raw

Rumur

Rumur is a model checker, a formal verification tool for proving safety and security properties of systems represented as state machines. It is based on a previous tool, CMurphi, and intended to be close to a drop-in replacement. Rumur takes the same input format as CMurphi, the Murphi modelling language, with some extensions and generates a C program that implements a verifier.

A more extended introduction is available in doc/introduction.rst

Quickstart

Installation on Ubuntu or Debian

apt install rumur

Installation on FreeBSD

pkg install rumur

Thanks to yuri@FreeBSD for packaging.

Building from Source

First you will need to have the following dependencies installed:

Then:

# Download Rumur
git clone https://github.com/Smattr/rumur
cd rumur

# Configure and compile
cmake -B build -S .
cmake --build build
cmake --install build

# Generate a checker
rumur my-model.m --output my-model.c

# Compile the checker (also pass -mcx16 if using GCC on x86-64)
cc -std=c11 -march=native -O3 my-model.c -lpthread

# Run the checker
./a.out

Compilation produces several artefacts including the rumur binary itself:

  • rumur: Tool for translating a Murphi model into a program that implements a checker;
  • murphi2c: Tool for translating a Murphi model into C code for use in a simulator;
  • murphi2murphi: A preprocessor for Murphi models;
  • murphi2smv: Tool for translating a Murphi model into NuSMV input;
  • murphi2uclid: Tool for translating a Murphi model into Uclid5 input;
  • murphi2xml: Tool for emitting an XML representation of a Murphi model’s Abstract Syntax Tree;
  • librumur.a: A library for building your own Murphi model tools; and
  • include/rumur/: The API for the above library.

Comparison with CMurphi

If you are migrating from CMurphi, you can read a comparison between the two model checkers at doc/vs-cmurphi.rst.

Legal

Everything in this repository is in the public domain, under the terms of the Unlicense. For the full text, see LICENSE.