Here we give an overview of the Kit's use. For that purpose the comments are structured into the following parts:

• Outline of the Kit
• Checking deadlock-freeness
• Checking reachability properties
• Checking safety and liveness properties
• Save and resume intermediate results

Outline of the Kit

The main program of the Kit is called check. Calling the program without arguments will display the usage (reproduced below).

check -- main program of The Model Checking Kit

Usage: check [options] <input>:<checker> <modelfile> <formulafile>
   or: check -r <name> [options] <checker> <formulafile>

     Options:
      -s <name>         save intermediate results under <name>
      -r <name>         resume from intermediate results saved under <name>
      -t <dir>          place temporary files in <dir> (default is '.')
      -o <opt>          specify options to pass to checker
      -v                run in verbose mode

     Available input formats:
      cfa               concurrent finite automata
      bpn2              B(PN)^2 language
      if                IF language
      pep               PEP low level net format
      senil             SENIL net format
      apnn              APNN net format

     Available algorithms:
      CTL         : prod-ctl, smv-ctl, dssz-ctl, lola-ctl
      LTL         : prod-ltl, pep-ltl, spin-ltl, dssz-ltl
      Deadlock    : prod-dl, smv-dl, pep-dl, mcs-dl, clp-dl, lola-dl
      Reachability: prod-reach, pep-reach, mcs-reach, spin-reach, lola-reach

Version 1.3.0 (17.03.2004)

• Usage:

For a correct program call one has to type:

check [options] <input>:<checker> <modelfile> <formulafile>
• The options are explained here.


• <input> is a place holder for one of the available modelling languages and should be replaced by one of bpn2, cfa, if, pep, senil, or apnn.
  Note: <input> may be omitted; in this case check guesses the input language by looking at the <modelfile>'s extension (which should be .bpn2, .cfa, .if, .ll_net, .senil, or .apnn, in the order of the languages mentioned above). You are free to use arbitrary extensions, but then you'll have to specify the language explicitly.


• <checker> should be replaced by one of the available algorithms, e.g. prod-dl, pep-reach, smv-ctl, or dssz-ltl (see above for the full list).


• <modelfile> is the name of the file containing the system specification.


• <formulafile> is the name of the file containing the formula that is to be checked.
• Options:
• -s <name>

Temporary files representing intermediate results will be saved in a tar archive mckit_save_<name>.tar. There are some algorithms which profit from the reuse of intermediate results. For example, if one uses a method based on the unfolding technique for verifying many properties on the same system, it is sensible to calculate the unfolding only once and not for every property over and over again. So the unfolding can be saved with this option for reuse (see option -r). See here for an example.
• -r <name>

With this option one can reuse intermediate results saved before with option -s <name>. This is sensible if one wants to check many properties on the same system. Then the translation from the modelling language into the correct input format for the checker should be done only once and not for every property over and over again. When using this option one should omit the modelling language and the modelfile. Then the correct program call is:
check -r <name> [options] <checker> <formulafile>

One can choose all those checkers taking advantage from the files saved in mckit_save_<name>.tar. See here for an example.

• -o <opt>

Many model checkers allow to influence their behaviour with a variety of options. The Kit uses every tool with a general-purpose set of options recommended by the authors, which is usually fine for educational purposes. Expert users of the Kit, however, may want to use the full power of the tools. The Kit passes the value of <opt> on in the call to the chosen model-checker, and its meaning depends on that tool.
• -t <dir>

Temporary files will be placed in the directory <dir>.
• -v

The program outputs additional information.

• Modelling languages:
• APNN (Abstract Petri Net Notation)

A language for the description of different classes of Petri nets. Keywords are similar to LaTeX commands.
• B(PN)² (Basic Petri Net Programming Notation)

A structured parallel programming language, offering among others loops, blocks and procedures.
• CFA (Communicating Finite Automata)

A language for the description of finite automata communicating through shared variables or channels of finite length. CFA offers very flexible communication mechanisms. It is one of the modelling languages of the PEP tool.
• IF (Interchange Format)

A language proposed in order to model asynchronous communicating real-time systems.
• PEP (Low level PEP notation)

A low level language, to be used by machines. It is included in this list only because some tools can export models in this language.
• SENIL (Simple Extensible Net Input Language)

Another language for the description of 1-safe Place/Transition Petri nets. Suitable for small nets having at most some dozens of nodes, but not for larger projects. Designed to be used by students.

• Algorithms:

The available algorithms are structured in four classes:
(A short introduction to each method is given here.)

• Checking deadlock-freeness:

mcs-dl		(Unfolding techniques)
pep-dl		(Unfolding techniques)
prod-dl		(Stubborn set techniques)
smv-dl		(Symbolic techniques)
clp-dl		(Unfolding techniques)

• Checking reachability properties (state formulae):

mcs-reach		(Unfolding techniques)
pep-reach		(Unfolding techniques)
prod-reach		(Stubborn set techniques)

• Checking CTL-formulae:

prod-ctl		(Explicit construction of the state space)
smv-ctl		(Symbolic techniques)
dssz-ctl		(Symbolic techniques)

• Checking LTL-formulae:

pep-ltl		(Unfolding techniques)
prod-ltl		(Stubborn set techniques)
spin-ltl		(Explicit construction of the state space)
dssz-ltl		(Symbolic techniques)

Checking deadlock-freeness

The Kit offers several algorithms for checking deadlock-freeness of a system. It returns YES if the system is deadlock-free. Otherwise the Kit returns a deadlocking execution sequence interpreted in the dialect of the corresponding modelling language. When checking a system for deadlock-freeness, no formula file is needed and so one must omit it.

• Usage:
check [options] <input>:<dl-checker> <modelfile>
• The options are explained here.


• <input> is a place holder for one of the available modelling languages and should be replaced by bpn2, cfa, if, pep, senil, or apnn.


• <dl-checker> should be replaced by one of the available algorithms for checking deadlock-freeness, namely prod-dl, smv-dl, pep-dl, mcs-dl, or clp-dl.


• <modelfile> is the name of the file that contains the system specification.

• Example:
  check senil:pep-dl dekker.senil

  The following output should be printed on your screen:

  Time needed: 0.020000 seconds
Result: YES.

Checking reachability properties

The Kit offers several algorithms for checking reachability properties specified as state formulae. State formulae are propositional logic formulae consisting of atomic propositions and logical operators. Generally speaking, one is interested in the question if there exists an execution sequence leading to a global system state which satisfies a given property. In this case the Kit returns YES and displays an execution sequence leading to such a global state in terms of the modelling language. Otherwise the Kit outputs NO.

• Usage:
check [options] <input>:<rc-checker> <modelfile> <formulafile>
• The options are explained here.


• <input> is a place holder for one of the available modelling languages and should be replaced by bpn2, cfa, if, pep, senil, or apnn.


• <rc-checker> should be replaced by one of the available algorithms for checking reachability properties, namely prod-reach, pep-reach, or mcs-reach.


• <modelfile> is the name of the file containing the system specification.


• <formulafile> is the name of the file containing the state formula to be checked.

• Example:
  check senil:pep-reach dekker_non_mutex.senil mutex.form

  The following output should be printed on your screen:

  Time needed: 0.110000 seconds
Result: YES.
Witness: "flag1:=1", "flag2=0", "flag2:=1", "flag1:=0"

In this example the specification of Dekker's mutex algorithm is changed in such a way that the mutex property is violated. The processes can enter their critical regions at the same time, and therefore the algorithm returns YES and delivers an execution sequence leading to a global state that is in violation of the mutex property.

For more details see here.

Checking safety and liveness properties

Safety and liveness properties are expressed in terms of temporal logics like CTL and LTL. We support these because they are the most popular temporal logics, and together they can express all common safety and liveness properties. The Kit offers several algorithms for proving properties formulated as CTL or LTL formulae. It return YES if the property holds. Otherwise the Kit returns NO and (possibly) outputs a counterexample.

• Usage:
check [options] <input>:<md-checker> <modelfile> <formulafile>
• The options are explained here.


• <input> is a place holder for one of the available modelling languages and should be replaced by bpn2, cfa, if, pep, senil, or apnn.


• <md-checker> should be replaced by one of the available model-checkers, that is prod-ctl, smv-ctl, dssz-ctl, prod-ltl, spin-ltl, pep-ltl, or dssz-ltl.


• <modelfile> is the name of the file containing the system specification.


• <formulafile> is the name of the file containing the formula that should be checked.

• Example:
  check senil:smv-ctl dekker.senil cr1entry.ctl

  The following output should be printed on your screen:

  Time needed: 0.040000 seconds
Result: YES.

For Dekker's mutex algorithm we have checked whether process 1 can enter its critical region over and over again. We have specified this property as a CTL formula.

Save and resume intermediate results

Some algorithms can profit from the reuse of intermediate results:

• pep-reach
• pep-dl, mcs-reach, mcs-dl, clp-dl     (using the same intermediate results)
• prod-ctl

For example, the algorithms pep-dl, mcs-reach and mcs-dl are all based on the unfolding technique. If someone wants to verify many properties on the same system with these algorithms, it is reasonable to calculate the unfolding of the system only once and not for every property or algorithm again. So the unfolding of the system can be saved, and later it can be reused for further verification tasks. Therefore, if someone is interested in verifying many properties on the same system using one of the methods mentioned above, it is sensible to save the intermediate results with the -s <name> option. Then a tar archive named mckit_save_<name>.tar will be created. For checking more properties on the same system one can proceed with the intermediate results using the option -r <name>. This step should speed up the verification procedure.

Now we show the correct use of both options by an example:

• check -s example senil:prod-ctl dekker.senil cr1entry.ctl

The following output should be printed on your screen:

Time needed: 1.200000 seconds
Result: YES.

• check -r example prod-ctl cr1entry.ctl

The following output should be printed on your screen:

Time needed: 0.010000 seconds
Result: YES.

• check -r example prod-ctl mutex.ctl

The following output should be printed on your screen:

Time needed: 0.010000 seconds
Result: YES.