Each MSC diagram defines some partial order on the set
of events, which can happen during its execution. This ordering must be
consistent with time specifications, which should not destroy the original
partial order of untimed MSC. This condition is known as time consistency of a
diagram.
To check time consistency symbolic simulation of a
diagram is used. In this case the state variables are time variables corresponding
to the moments of time when events happen. The simulation of a diagram
generates traces. Each trace defined by simulating a diagram is a sequence of
events. Let this sequence be s1,
s2, … , and let v1, v2, … be the moments of time when events happen. The
constraints for these time variables can be generated from time specifications.
Each constraint in the simple case has the form vi = vj + xi & ai ≤ xi ≤ bi, where j < i and j depends on a type of time specification, xi is an
auxiliary variable which defines possible shifts of the time vi relative to the time vj. Note that there are four
types of time specifications :
1.
Absolute time. In this case vj = 0.
2.
Relative time. In this case vj is the time of a previous event on the same instance.
3.
Labelled time specification defined by a given label l. In this case vj is the time of event labeled by l.
4.
In-message specification. In this case vj is the time of
corresponding out-message event.
More complex constraints have the form vi = max{ vj1, vj2,…}
+ xi
& ai
≤ xi ≤ bi . They correspond to
events that follow conditions and are explained by synchronization semantics of
conditions. Let E be the conjunction
of all constraints for a given trace. Let s
and s' be two neighboring events
located on the same instance, s'
follows s, v and v' are the moments
of time corresponding to these events. Then the inequality v ≤
v' must be logical consequence of constraints E. This is the exact formulation of time
consistency problem. The problem is reduced to the solving of linear constraint
systems (equalities and inequalities) over reals and a special prover and
solver are used to implement a method for solving time consistency problem.