Modex can be used to mechanically extract verification models from implementation level C code. The model extractor is guided by a user-defined test-harness, specified in a separate file with extension ".prx". The format used in test-harness files is documented in a companion user-guide.
For a description of, and some references to, early applications of this tool at Bell Labs between 1998 and 2000, see the pointers at the bottom of this page.
The following installation instructions assume you are working on a Unix/Linux or comparable system (e.g., Ubuntu). On a Windows PC, a cygwin distribution is assumed, which is freely available from http://www.cygwin.com/.
InstallationThe modex sources were first released for general distribution by Bell Labs/Lucent Technologies in November 2002. A first web-distribution was prepared in January 2003. The current distribution is Modex Version 2.1 from November 2012.
You can install the code as follows.
Create a directory for the new installation, e.g.
mkdir ~/modexand copy the distribution archive into that directory:
$ mv modex_2.X.tar.gz ~/modex $ cd ~/modex $ tar -xzvf modex_2.X.tar.gz # unpack the archive $ cd Src2.X $ make install # you may need to sudo thisYou may first want to edit the makefile in the Src directory, for instance to adjust the desired installation directory, or the C compiler to be used. You will minimally need the following tools to be able to compile Modex: gcc, bison (or any other version of yacc), and flex (or any other version of lex).
To use modex you must also have a reasonably recent version of Spin installed. To check which version you have, type:
$ spin -V Spin Version 6.2.2 -- 6 June 2012If you have an old(er) version, or no Spin version at all, you can download and executable copy, or a source package from:
$ cat Examples/README.txtThere is a script named verify in the Scripts directory that can simplify working with Modex. Copy it in the bin directory, for instance as:
$ cp Scripts/verify /usr/local/bin
With the verify script (and with a .prx file in place) you can then simply say:
$ verify arb.c # perform model extraction + verification $ verify clean # clean up temporary files
|(last update: 15 December 2013)|