Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
SZS | Contact | People | Teaching | Research | Publications | Tools | Institute | Department | Links
Institute of Formal Methods in Computer Science

Model-Checking Kit: Describing properties
 

Several types of properties can be checked, e.g. deadlock-freeness, reachability, safety and liveness properties. Except for deadlock-freeness these properties will be expressed as formulae. Therefore, this page is structured in two parts:

 

Describing reachability properties

First we shortly explain our notion of reachability property. It is a statement about states of the system. For example, the mutual exclusion property of critical regions can be understood as reachability property it amounts to the question if there exists a reachable global state of the system in which two processes have entered their critical regions at the same time. These properties can be expressed with so-called state formulae. A state formula is a propositional logic formula consisting of atomic propositions and logical operators. Details about the syntax are shown here.

 

Describing safety and liveness properties

Safety and liveness properties will be expressed in terms of temporal logics like CTL and LTL. They are the most popular logics, and together they can express all common safety and liveness properties. A detailed syntax of CTL and LTL is shown here. We shall give a short introduction to LTL and CTL according to [EME90]:

  • LTL
    means Linear Temporal Logic. Here the underlying structure of time is a totally ordered set. In the following the time corresponds to (N, <). Under this assumption the time is discrete, has an initial moment with no predecessors and is infinite into the future. LTL formulae consist of atomic propositions, boolean connectives and temporal operators. Temporal operators are Gp ("always p", "henceforth p"), Fp ("sometime p", "eventually p"), Xp ("nexttime p") and pUq ("p until q"). The figure below illustrates their intuitive meanings:

    Remark:
    The algorithms offered by the Kit support only the next-free fragment of LTL.

  • CTL

    • is closely related to branching time logics. The underlying structure of time is assumed to have a branching tree-like nature. It corresponds to an infinite tree where each node may have finitely many successors and must have at least one successor. These trees have a natural correspondence with the computations of concurrent systems or nondeterministic programs. A CTL formula consists of a path quantifier [A (all paths ...), E (it exists a path ...)] followed by an arbitrary linear-time formula, allowing Boolean combinations and nestings of linear-time operators (G, F, X, U).

Selected References

[EME90]  
  E. A. Emerson. Temporal and Modal Logic. Handbook of Theoretical Computer Science, vol. B, pages 997 - 1067, Elsevier Science Publishers B. V., 1990.

Next chapter: Checking properties

 
last change 08.05.2003 (mailto cs) |  © University of Stuttgart | legal notice