Modex/FeaVer - Version 1.0 - January 2003

MODEX README

Introduction

Modex is a tool that can be used to mechanically extract high-level verification models from implementation level C code. Modex itself is written in ANSI-C, and its application domain is also restricted to ANSI-C code (i.e., it does not handle C++). The model extractor is guided by a user-defined test-harness, which is specified completely in a separate file with the extension ".prx". The format used in test-harness files is non-trivial and, like any other language it has to be learned before you can use it. See the section on Documentation below to find out more. Model extraction and abstraction are also very much still in the domain of research, not of push-button application. So, as a minor disclaimer, if you plan to use these tools, be prepared to spend some time to learn how everything is meant to work. The documentation gives a good head-start. Experience with the application of the tools, building test harnesses, and verifying applications, will do the rest. Experience with the effective use of these tools comes slowly but surely, so be patient! After these somewhat discouraging notes, it is also good to add that the reward for finally mastering the use of these tools can be very substantial. Our own experience to date indicates that these tools, if used right, allow us to verify software applications, or portions thereof, with a thoroughness that cannot be achieved by any other testing or verification method.

For a description, and some references, on some early applications of these techniques at Bell Laboratories between 1998 and 2000, see the pointers to related software at the bottom of this page.

The following installation instructions assume you are working on a Unix or comparable system.
On a Windows PC, the cygwin distribution is assumed, which is not only recommended but also freely available from www.cygwin.com.

So what is the difference between AX, Modex, FeaVer and Spin...?

The name for the tool that is part of this distribution is Modex, which is an acronym of Model Extractor. Before being christened like this, the tool lived short lifes as Pry, Catch, and it has also often been referred to as as AX (short for Automata eXtractor). The name MOX was also considered for a short while, as was MCC (Model Checker for C programs), until we finally settled on Modex towards the end of 2000.

FeaVer was originally the name of the system we built for the analysis of the PathStar call processing code in 1998 and 1999. Later we made the software independent of this first application, and reserved the name FeaVer for the user-interface to the model extraction and verification tools. FeaVer, then, is much like Xspin in that it helps the user to synthesize commands to background tools that do the real work. In the case of FeaVer the background tools include the model extractor Modex, the logic verifier Spin, the C preprocessor and compiler, and a couple of Unix-style postprocessing commands.

Installation

These sources were released for distribution by Bell Laboratories/Lucent Technologies in November 2002. The first web-distribution was prepared in January 2003. The current version is from August 2005, with some minor fixes.

Before installing, please read the license text for this distribution and make sure you find nothing problematic. This distribution is covered by this general Lucent, non-exclusive source code license: 

	SourceLicense.txt
Assuming that you agree with these general terms, you can download and install the code as follows.

First, create a directory for the new installation, e.g. 

	mkdir /usr/local/modex
and download the distribution archive to that directory: 
	modex.tar.gz
proceed as follows to compile and install the software ($ is the shell prompt below): 
	$ cd /usr/local/modex
	$ gunzip modex.tar.gz	# gnu unzip
	$ tar -xvf modex.tar	# unpack the archive
	$ cd Src
Edit the makefile in the Src directory, for instance to adjust the desired installation directory, and the C compiler to be used - it defaults to gcc. Read the instructions at the top of the makefile to see what other installation directories need to be defined. You will minimally need the following tools to be able to compile Modex: 
	bison
	flex
	gcc
Then continue with: 
	$ make install
Next, to run the tool you must have Spin Version 4 installed. To check which version you have, type: 
	$ spin -V
	Spin Version 4.0.2 -- 12 January 2003
If you have an older version, or no Spin version at all, you can download and executable version, or a source package, of this tool from: 
	http://spinroot.com/spin/Bin/index.html
To test if your installation works, cd to the Examples directory and check the README.txt file there: 
	Examples/README.txt
There are two scripts in the Scripts directory that can greatly simplify working with Modex: a simple shell script for command line use, and a graphical user interface. Start with the command line script to become comfortable with what Modex does, or tries to do, before playing with the GUI.

User Guide

Documentation of Modex/FeaVer is available in the user guide in the Doc directory: 
	Doc/feaver.pdf
Read at least the documentation through once to know what the tool tries to accomplish, and what stumbling blocks you may be encountering if you try to use it on new applications. Inspiration for new applications can be found in the Examples directory. Look carefully at how the test-harnesses are constructed.

Publications about Modex/FeaVer

Related Software

(Page Updated: 9 August 2005)