1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
Tool for UML Activity Diagrams (TATD).
----------------------------------------------
This tool is intended for UML activity diagrams (ATDs).
More about the drawing of ATDs can be found in chapter 5 of the
user's guide and more about the use of this notation technique
can be found in appendix A of the user's guide.
TATD supports model checking. More information about model
checking can be found below.
Diagram editing in general.
---------------------------
Diagrams that are made by a diagram editor are a special
kind of graph consisting of nodes and edges and with a certain
representation. In the representation of a graph, nodes and edges are
shown as shapes (boxes, lines, diamonds etc.).
Documents should satisfy certain constraints. Most constraints
are specific for the particular diagram technique supported by the
editor. In the editors there are three kinds of constraints:
1. Built-in constraints which are constraints which can never be
violated because there is no command in the user interface to achieve
that.
2. Immediately enforced constraints: when you perform a command that
would violate a constraint that is immediately enforced, this command
is rejected immediately by the editor and a pop-up window with an error
message is displayed.
3. Soft constraints which are constraints that can be violated.
Soft constraints are checked by the editor when the Check Document
from the Document menu is issued by you. Check Document displays a list
of error messages in a pop-up window. As opposed to the previous two
classes of constraints, you are responsible for correcting the diagram.
Model checking.
---------------
With model checking, one can automatically verify whether or not an
activity diagram satisfies a particular requirement, given by the user.
If the activity diagram fails to satisfy the requirement, the counter-
example returned by the model checker is highlighted in the diagram.
Some entries under the Document menu are related to model checking.
- Model Check Property: a popup dialog box appears in which you can type
a temporal logic formula (LTL or CTL). If you refer to a node n in the
diagram, use `in(n)' in your formula. Checkbox `syntactic encoding'
means that the syntax of activity diagrams is encoded directly as input
for the model checker. THIS ONLY WORKS FOR SAFE ACTIVITY DIAGRAMS. TCM
DOES NOT CHECK WHETHER OR NOT AN ACTIVITY DIAGRAM IS SAFE.
Checkbox `reduction' means that the activity diagram is reduced (without
sacrificing the truth value of the property!), before feeding it to the
model checker. Checkbox `strong fairness' means that every loop is exited
eventually. Preferred usage: check `reduction' and `strong fairness'.
- Clear Trace: undo the highlighting of the counterexample trace.
|
