Time Features in SCStudio
Ľuboš Korenčiak
14. 11. 2011
Ufa* I       "XSr    £3 (B)
.—^^ ■ fOC'al"L„ MINISTERSTVO ŠKOI STVi. OP Vzdělávaní Jv^i^jS*
■^^^ ■    fOndvCR    EVROPSKAUNIE      MLÄOĽŽĽ A TĚLOVÝCHOVY      pro konkurenceschopnost l«4JÍA**
INVESTICE DO ROZVOJE VZDĚLÁVÁNÍ
řT. ACSD 2012 - Microsoft Visio | •=> || 1Š1 MéMI
File   Edit  View  Insert   Format  SCStudio  lools   Data   Shape  Window   Help    Type a cucstion fcr help 0 X
1 □ T       Ö   Ö 400%				- ! Arial			L2pt												' -		» ~H L ar				B		
Shapes         - X																											
Search for bhapes: lypeytiur Sf w |^																											
ll Jd; . MSC					Peter															Jane							
f— Instance																											
					1																	I					
																											
J   ; CorcgOn -4— Headless !•— instance											1-	i;		I'm		Peter											
												II															
																											
																											
									Will you						marry			f	me?								
1.      1 Message ™i (Left)																											
																				f							
																											
1     .1 Message i      i (Right)																											
																											
LOSl																											
Message																											
																											
-   J hound Message																											
																											
																											
																											
■(   |   ) condtion																											
																											
		4	► W	s( studio Poster																							
basic Message Sequence Chart (BMSC)
Lbmsq = {(p\q, 1)(<7?P, 2)(q\p, 3)(p?q, 3),...}
Time Consistency
Algorithm checks whether introduced time constraints are in conflict.
There is no execution which could satisfy all time constraints.
Tightening
BMSQ
p q
The purpose of Tighten Time algorithm is to "tighten"the constraints to contain only values which are possible in at least one execution.
Tightening
BMSQ
p q
The purpose of Tighten Time algorithm is to "tighten"the constraints to contain only values which are possible in at least one execution.
Time Race
Race condition is a property when events are drawn to take place in some order but they can take place in different order.
The introduction of time constraints can eliminate some race conditions.
Time Race
Client A Proxy Server Client A Proxy Server
r~  i        i  ;  i        r~  i i  ;  i        i  ;  i \—
Solving of Tightening
Translation to the Temporal Constraint Satisfaction Problem (TCSP).
BMSQ
Solving of TCSP
• translation to oriented graph
• shortest paths
• Floyd-Warshall
Luboš Korer
Solving of TCSP
• x := max{x, y + z}
• x' := min{x',y' + z'}
• y := min{y,x — z'}
• y' := min{y', x' — z'}
Luboš Korer
Summary
• introduction of timed MSC
• definition time problems
• solving of time problems
evropský
fOndvČR     EVROPSKÁUNIE  M m'á JtitA1 l'i.!u^íCHOVY pinko"
INVESTICE DO ROZVOJE VZDĚLÁVÁNÍ
m