Model-Checking Kit

university

sitemap

contact

legal notice

University of Stuttgart

	Institute of Formal Methods in Computer Science
	Model-Checking Kit: Adding a new checker

Introduction

The functionality of the kit can be stated like this:

Input:

A system in one of the available modelling languages.
A property of the modelled system (CTL or LTL).
or: the question "Is the system deadlock-free?"
or: a reachability question.
A specification which checker should be used for verification.

Output:

A result (yes/no - property holds/does not hold), and possibly a witness / counterexample path generated by the selected checker. In order to make the results meaningful, witness/counterexample paths should be represented as runs of the modelled system (i.e. not as runs of its Petri net semantics!).

Examples:

Input: a Petri net, a formula "P1 and P2 will never be marked at the same time". Ouput: Yes/No, possibly a sequence of transitions.
Input: a system of communicating finite automata (CFA), a formula "eventually, x will hold the value 2". Output: Yes/No, possibly a sequence of state transitions in the automata.

As you can see, our aim is to hide from the user the necessary translation of the modelled system into the checker's language. To make this approach work with all the languages and checkers we need a common intermediary format of the input data.

Overview

In order to add a new checker to the Kit you need to implement a function that checks the validity of a formula with respect to a system. The system is given in an intermediary Petri net format (see the corresponding section in the other chapter), and the formula makes a statement over this net.

The following kinds of checkers are present in the Kit:

CTL model-checkers
LTL model-checkers
Deadlock checkers
Reachability checkers

Any new checkers that are implemented should fit into one of these categories.

Details

The list of supported checkers/algorithms is held in the array output_types in main.c. A new checker is added to the Kit by extending this array by another entry. The format of the entries in output_types is explained in greater detail in formats.h. The most important data field is a pointer to the function that runs the algorithm:

result_t (*checkfunc)(net_t,tree_t)

This function acts as the "driver" for an algorithm. It takes as arguments a net and a formula. It should examine whether the formula holds for the given net, and return the result. The function may return NULL to indicate that an error has occurred. Note: For deadlock checkers, the formula argument can be ignored (it is NULL).
The data structures used for storing nets and formulae are defined in netconv.h and tree.h, respectively.
The sets of places and transitions of the net are stored in simple lists of type list_t. This data type is defined in list.h. The for_list macro allows you to iterate over all the elements in a list.
tree_t is a binary tree structure used for storing a formula. Internal nodes are inscribed with operators, while leaf nodes are inscribed with places (of the net). The meaning of such a leaf is "the place associated with this leaf is marked".
The functions task is to evaluate the formula's validity. How this task is accomplished is entirely in your own responsibility. All the current algorithms work by writing both the net and the formula into files and running some external program. External programs should be called with nc_run (implemented in netconv.c); direct use of system() is deprecated.
The function output_formula in tree.c goes through a formula tree and prints its contents to a stream. The exact output can be customized, so this function may save you a bit of work.
While the algorithm is running you may want to print messages to the screen, e.g. to inform the user about what is currently going on. Please do not use printf directly; use the functions nc_info, nc_print and nc_error instead. These are implemented in netconv.c and emit messages to the standard output or standard error stream. All of these functions can take multiple arguments just like printf does. Using these functions is encouraged because later versions of the tool may want to redirect or filter the output.
The function should return a data structure of type result_t (which is defined and explained in greater detail in netconv.h). A new, empty structure can be generated by nc_create_result. Most importantly, a result_t struct contains the field holds (designed to take the yes/no answer) and the field example which is a list that can hold a sequence of transitions in the intermediary net. This can be used for giving a firing sequence that witnesses or falsifies the formula.
example is of type list_t (see above). You can add elements to the list with list_add (defined in list.c). Since this list is supposed to hold a sequence of transitions, it is assumed that the elements in it are of type node_t.

Example:

prod.c contains drivers for the algorithms related to SMV. The function write_prod_net demonstrates a simple conversion of the intermediary net format into a PROD net. It also demonstrates how you can iterate over the places and transitions in a net using for_list.
convert_to_prod_ltl in combination with eval_prod_gen is an example for a driver function; here, both net and formula are converted into PROD input, then PROD is called as an external program, and finally the result is evaluated and placed into a result_t struct.
In smv.c, write_smv_formula shows how to make use of output_formula.