What is it?

Here you can find an extension of TATD, a tool to draw UML activity diagrams, with verification support using model checking. The verication support is intended for activity diagrams that model workflows. The workflow models can have loops, data, and real-time and are event-driven. The actual verification is done by NuSMVfair, an extension of the NuSMV  model checker with strong fairness model checking. NuSMVfair is part of NuSMV versions 2.1 and higher. So to do the actual verification you must get NuSMV 2.1 or higher as well. TATD automatically translates any error trace the model checker return back in terms of the original activity diagram by highlighting a corresponding path through the diagram. The semantics that the tool implements is defined in an earlier paper,  see also my Ph.D. thesis.
 

How can I get it?

To obtain TATD with model checking do the following:
  1. get the 2.10 source distribution of TCM ;
  2. follow the build instructions for TCM. Usually, a `make config' in the top directory, followed by a `make libs' and a `make tatd' suffices for building TATD.
NuSMVfair can be obtained by downloading NuSMV 2.1 here.
 

How do I use it?

The resulting executable TATD works similar to the orginal version TATD executable, except that it has an extra menu item `Model check property' under `Document'.  If this new menu item is chosen, a pop-up dialog appears in which the user can write a formula in Linear Temporal Logic(LTL). The LTL formula must be according to the following grammar:

ltl_formula ::=  p
         | INITIAL
         | FINAL
         | TRUE
         | FALSE
         | stable
         | IN(node name)
         | G formula
         | F formula
         | X formula
         | formula U formula
         | (formula)
         | formula & formula
         | formula | formula
         | ! formula
         | formula -> formula
         | formula <-> formula

where p is an event or a guard condition that appears in the activity diagram. Predicate INITIAL is true iff the current state (valuation) only contains an initial state node. Predicate FINAL is true iff the current state (valuation) only contains final state nodes. Predicate stable is true iff the current state is stable, i.e., there are no events and no enabled edges.
Note: the tool does not automatically insert the stable predicate in a formula; you have to  do this yourself!

Currently, also a restricted subset of Computation Tree Logic (CTL) is supported. The used CTL formula's are described by the following grammar.

ctl_formula ::=  p
         | INITIAL
         | FINAL
         | TRUE
         | FALSE
         | stable
         | IN(node name)
         | AG formula
         | AF formula
         | EG formula
         | EF formula
         | (formula)
         | formula & formula
         | formula | formula
         | ! formula
         | formula -> formula
         | formula <-> formula

Please note that NuSMV forbids the following identifiers

A,AF,AG,AX,E,EF,EG,EX,F,G,U,X

So in the grammar above, p and node name cannot be equal to either of these identifiers.
Spaces in node names are allowed, but not recommended.

TATD translates an error trace that the NuSMVfair model checker returns, automatically back into the diagram by highlighting some path in the diagram that corresponds with the error trace.

The Figure below  gives the semantics of the temporal operators G(lobally), F(uture), U(ntil) and X (next). Circles denote states of the Kripke structure. A symbol x in a circle denotes that x is true in that state. If x is not in the circle, then x is false in that state. A dash (-) in a circle, denotes that it does not matter what the valuation of the symbols in that state is.

More information on temporal logic can be found in the NuSMV user manual and at the TLV homepage.
 

Background

The most uptodate background can be found in my Ph.D. thesis.

Here is a report describing the implementation and how to use it (last updated 17 october 2001).

Publications on (formal) workflow modelling with UML activity diagrams.
 
 
 

Examples

to appear...

Rik Eshuis (eshuis @ cs.utwente.nl) , 31-10-2002