MODEX README

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/.

Installation

The 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.10 from June 24, 2017.

You can install the code by cloning the GitHub/Modex distribution and typing make: 

	$ cd Modex/Src
	$ make install	# you may need to sudo this
You may first want to edit the makefile in the Src directory, for instance to adjust the target installation directory, or the C compiler to be used. You will 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 recent version of Spin installed. To check which version you have, type: 

	$ spin -V
	Spin Version 6.4.6 -- 2 December 2016
If you have an old(er) version, or no Spin version at all, you can find the source code and documentation at GitHub/Spin, and binaries (if you don't want to compile it from the sources) at: 
	http://spinroot.com/spin/Bin/
To test if your installation works, cd to the Examples directory and check the README.txt file there: 
	$ cat Examples/README.txt
There 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

Publications

  • 1999:
    • G.J. Holzmann and M.H. Smith, A Practical Method for Verifying Event-Driven Software Invited Paper. Proc. ICSE99 International Conference on Software Engineering, Publ. IEEE/ACM. May 1999, Los Angeles, pp. 597-607.
      icse99.pdf
    • G.J. Holzmann and M.H. Smith, Software Model Checking: Extracting verification models from source code Formal Methods for Protocol Engineering and Distributed Systems, (Conference Proceedings FORTE/PSTV99), Kluwer Academic Publ., Oct. 1999, pp. 481-497.
      fortepstv99.pdf
  • 2000:
    • G.J. Holzmann, Lecture Notes on Software Model Checking, Nato Summerschool, Aug. 2000, Marktoberdorf, Germany.
      marktoberdorf.pdf
    • G.J. Holzmann and M.H. Smith, Automating Software Feature Verification Bell Labs Technical Journal, Vol. 5, No. 2, April-June 2000, pp. 72-87.
      bltj2000.pdf
    • G.J. Holzmann, Logic Verification of ANSI-C Code with Spin Proc. SPIN2000, Springer Verlag, LNCS 1885, pp. 131-147.
      spin2000.pdf
  • 2001:
    • G.J. Holzmann and M.H. Smith, Software Model Checking: Extracting verification models from source code Software Testing Verification and Reliability, Vol. 11 No. 2 June 2001 pp. 65-79.
      (A journal version of the Forte/PSTV99 paper.)
    • G.J. Holzmann, From Code to Models, Proc. 2001 Int. Conf. on Applications of Concurrency to System Design, 25-29 June 2001, Newcastle upon Tyne, England.
      code_models.pdf
  • 2002:
    • G.J. Holzmann and M.H. Smith, An automated verification method for distributed systems software based on model extraction, IEEE Trans. on Software Engineering, Vol. 28, 4, pp. 364-377, April 2002.
      (An expanded journal version of the ICSE99 paper.)
    • D. Dams, W. Hesse, G.J. Holzmann, Abstracting C with abC, Proc. CAV 2002, Springer Verlag LNCS, Copenhagen Denmark, July 2002.
  • 2005:
    • G.J. Holzmann and T.C. Ruys, Tutorial at the 12th Spin Workshop in San Francisco. August 2005.

Related Software

  • Spin, the logic model checker used by FeaVer.
  • Swarm, a swarm verification front-end for Spin.
  • Uno, a simple static analyzer for C Code.
  • FeaVer, a description of the application of the model extraction technique to the verification of the PathStar call processing code between 1998 and 2000.
  • Cygwin, to setup a very workable Unix-like environment on a Windows PC.

(last update: 10 March 2019)