Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
Institute of Formal Methods in Computer Science

Model-Checking Kit: Adding a new language

 

Introduction

Basically, the functionality of the Kit can be stated as follows.

Input:

  • A system in one of the available modelling languages.
  • A property of the modelled system. Apart from atomic propositions the syntax of properties is supposed to be independent of the modelling language.
  • 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 integrate a new language into the Kit a new module must be implemented with three functions:
  • one function that returns the modelled system - i.e. by reading its specification from a file and generating its safe Petri net semantics;
  • one function that returns the property in question - i.e. by reading it from a file and generating a tree representation;
  • one function that presents the checker's result (given in terms of the Petri net semantics) to the user as a run of the modelled system.
For a better understanding of how these interrelate, let us briefly review the chronological order of events in the execution of the kit:
  1. Interpretation of command line arguments.
  2. Obtaining the modelled system.
  3. Obtaining the property.
  4. Running the checker.
  5. Interpretation of the result.
The functions of the new module correspond to items 2, 3, and 5 in this list.

The intermediary format mentioned above places a restriction on the kinds of input languages we may cover. We decided to allow languages that can be defined in terms of a safe Petri net semantics.

From this it follows that every system will (internally) be represented by a state/transition net, more precisely by:

  • a list of places;
  • a list of transitions;
  • a set of directed arcs between pairs of places and transitions;
  • an initial marking of the places.
Additionally, we provide a mechanism for storing extra information that might be useful for at least some checkers (like a partition on the set of places). However, extra information should be optional - the applicability of a checker should not depend on whether it understands the information. In other words, the semantics of the system should be contained completely within the data mentioned in the previous list.

It is worth noting that the intermediary Petri net format is not an additional file format; it exists solely as a data structure inside our program. The first function's task is therefore to construct such a data structure so that other parts of the program can access it.

In a similar way the representation of formulae (properties) is standardised; we are looking for a tree whose internal nodes are marked with logical and temporal operators, and whose leaves are marked with the name of places (of the intermediary net). A generic formula parser is provided so that programmers who add a new language just need to implement the translation of atomic propositions.

Details

The list of input languages supported by the Kit is defined by the array input_types[] in main.c. Technically, all that is required to add a new language is to add another entry to this array. The format of such an entry is explained in detail in formats.h. Apart from the fields name and suffix there are three function pointers that demand additional comments. These function pointers define the three functions mentioned in the Overview, in that order.
  • net_t (*readfunc)(char*)

    This function is called by main.c. Its argument is the modelfile given on the command line. The function should return the intermediary net representing the system modelled in the argument. The function may return NULL to indicate that an error has occurred.

    The structure net_t is defined in netconv.h. The file netconv.c contains useful operations on nets, among them:

    • creation of an empty net (nc_create_net)
    • creation of places and transitions (nc_create_{place,transition})
    • creation of arcs (nc_create_arc)

    Some more general routines are also contained in netconv.c:

    • nc_print (for printing important information to the screen)
    • nc_info (for printing information only to be displayed in verbose mode (-v)
    • nc_error (for printing error messages)
    Currently, these functions just print messages to stdout or stderr, respectively. However, it is encouraged to use these instead of plain calls to printf in case later versions of extensions of the program want to redirect/filter the output.

    Examples for this kind of function can be found in the input_types table in main.c, like read_pep_net, read_sen_net etc. The inner workings of such a function may vary - it's up to you. You might want to use some yacc/lex combinations, or even call external programs. The only important thing is that the function returns a net for further processing.

  • tree_t (*formfunc)(char*,net_t,int)

    This function takes the following kinds of arguments: The name of the formula file (as given by the user on the command line), the intermediary net under consideration and the kind of formula that should be checked. The third argument can take values of FORM_CTL, FORM_LTL, or FORM_REACH.

    The function should return a formula over the given net, or NULL if an error has occurred. The formula is expected to be returned as a binary tree as defined in tree.h.

    The syntax of formulae should be uniform across all input languages, Naturally, the set of atomic propositions may vary between different languages, but this should be the only difference - e.g., the set of (temporal and logical) operators and their syntax should be the same. To this end we provide a generic formula parser (formula.y). This parser is capable of reading all three kinds of formulae (CTL, LTL, and reachability), supports macros and can be customized to support propositions in multiple input languages. Although it is not a requirement we recommend that this parser be used.

    If you use the parser in formula.y, your work is reduced to coding a parser for atomic propositions. For more details read the comments in formula.y, and for an example take a look at read_generic_formula in generic.c.

    As stated previously the function should return the formula as a binary tree (see formula.y for examples how to construct such a tree). The tree's internal nodes should be inscribed with temporal and logical operators, and its leaves should be inscribed with pointers to places in the intermediary net. The meaning of such a leaf should be "the place inscribed upon this leaf is marked".

    tree_t is a data structure defined in tree.h. Some operations like create_tree or create_leaf are implemented in tree.c. The constants used for inscriptions of the nodes are taken from the automatically generated file formula.h.

  • void (*outputfunc)(net_t,result_t)

    This function is called after the checker has been run and the validity of the formula has been examined. The arguments given to the function are the net and the checker's result. The function is expected to present the result to the user - i.e. in such a way that a statement is made about the system originally modelled by the user. In other words, sequences of firing transitions in the intermediary net should be interpreted as a run of the original system.

    The structure result_t is defined and explained in netconv.h. Its most important data fields are holds (which assumes either NC_YES or NC_NO meaning that the formula holds/does not hold) and example which may hold a sequence of transitions which, if fired, provide a witness or a counterexample to the result.

    Examples for output functions can be found in the table in main.c. For Petri net languages like PEP, SENIL or APNN, the output function is trivial; for B(PN)2 and CFA things get more complicated.

    The counterexample/witness path is held in a list of type list_t. This simple, general-purpose list structure is defined in list.h. Elements of a list can be traversed using the for_list macro.