Time Consistence Help

       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  &  aixibi, 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  &  aixibi . 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.