======================= = BRIEF DESCRIPTION

This application is the attempt to implement model checking (verification and controller synthesis) for DTLHS. The main idea is using Fourier-Motzkin procedure to get rid of real variables and using NuSMV software to handle obtained system.

The latest version of this software is always available at http://github.com/darth/model_checking_hybrid/

======================= = AUTHORS

Our development team:

• Vadim Alimguzhin [email protected]

• Anton Bogin [email protected]

• Viktoriya Kozyreva [email protected]

• Denis Makartetskiy [email protected]

======================= = WHAT IS DONE

At this moment the following process is implemented:

1) read DTLHS from the input file;

2) eliminate output variables;

3) make quantization of DTLHS;

4) eliminate real parts of variables;

5) build equisatisfiable CNFs for the systems of linear constraints from DTLHS;

6) compose input file for NuSMV software;

7) launch verification using NuSMV;

8) read counterexample from xml file, if verification process fails.

======================= = TODO

Implement:

• building SMV model directly using CUDD OBDD package;

• working with NuSMV through its api;

• complete the whole chain (both verification and controller synthesis).

======================= = BUILDING

Prerequisites:

• GNU C++ compiler

• GNU make utility

• GMP library (with C++ bindings) http://gmplib.org/

• FM library Original version: http://www-rocq.inria.fr/~pouchet/software/fm/ We use modified version, it is available at: http://github.com/darth/fm_lib_with_gmp/

• Xerces-C++ library http://xerces.apache.org/xerces-c/

• Minisat+ http://minisat.se/MiniSat+.html We use slightly modified version, it is included in the sources (directory 'minisat+').

Run

% make release

for building release binary.

Run

% make debug

for building debug binary.

Run

% make

for building both of them.

Run

% make clean

for cleaning after (un)successful build.

======================= = USING

Prerequisites:

• NuSMV software http://nusmv.irst.itc.it/

Help for the application using can be obtained by invocation it with '-h' ('--help') parameter.

% ./project.exe -h

Prototype of model checker for hybrid systems 0.1 usage: ./project.exe [-v level] [-q value] filename read model from "filename" and verify with "value" of q_param or: ./project.exe -h print help message

If verbosity value is more than 0 result of intermediate steps are printed to the standard output.

Examples of input files are in the directory 'examples'. The format is simple and self-explaining.

======================= = DOCUMENTATION

Doxygen documentation can be obtained by running

% make doc

Doxygen software is needed for this step. Generated documentation will be in the 'doc' directory.

======================= = FILES

build/ Directory for object files for release binary.

build_debug/ Directory for object files for debug binary.

doc/ Directory for documentation.

examples/ Directory with sample input files.

minisat+/ Minisat+ sources.

src/ Directory with header and source files.

Doxyfile Configuration file for Doxygen.

Makefile Project's makefile.

README This file.

nusmv_cmds File with commands for NuSMV interactive mode.