CSML is a high level level language for describing finite state machines. There is a compiler which produces a finite state machine as output. There is also a CTL model checker called MCB which accepts the state machine file as input. MCB is an enhanced version of the EMC model checker. Both are available by clicking on the line below, or via anonymous FTP (user anonymous, password anonymous@host) on EMC.CS.CMU.EDU (128.2.250.142) in
pub/csml.tar.Z (230K) -
compressed tar file
csml.tar.gz
(131K) - gzipped tar file
Clicking on the reference above retrieves the file
automatically.
csml.tar.Z contains the sources and binaries for Sun 3, and VAX in "tar" format. To break out the directory structure, after you have gotten the file, use the commands
uncompress csml.tar.Z
tar -xf csml.tar
The package contains:
Each source directory contains a file READ.ME which
describes how to build the program(s). Particular attention should be paid to
the directions for compiling csml. The CSML compiler uses a macro preprocessor
called ltdmac, which in turn uses the C language preprocessor cpp. In the
makefile there is a definition which tells ltdmac where to find cpp on your
system. This should ordinarily be set to /lib/cpp. Also, the state machine
composer program smc has some parameters in its makefile which set limits on the
size of the composed state machine. If you want to construct very large state
machines, you will want to modify these.
There is a UNIX manual entry for the CSML compiler in the file csml/csml.1, and for the model checker in smc/smc.1. If you put these files in your man path, you will be able to get some documentation on-line.
CMU-SCS Model Checking home page