Information Technology Reference
T1: The data source arrivals are modeled with an rate of one frame every 50 ms.
T2: The next constraint states that successfully transmitted frames arrive at the data
sink between 80ms and 90ms.
˄ source_out → ଜ [80,90] sink_in ˅
T3: If the arrival rate the data sink is not within [15, 20]frames per second, then an
error should be reported.
( sink_in i ∧ ( ≤1000 sink_in i-21 ∨ ≤1000 ¬ sink_in i-15 )→Ο error )
T4: The final property states that if play is selected then it happens exactly 5ms after a
frame is received.
( sink_in i ∧ ( ଜ ≤1000 sink_in i-15 ∧ ଜ ≤1000 sink_in i-20 ଜ ≤1000 ¬ sink_in i-21 )→ ଜ d\G play )
The real-time constraints are transformed into the event scheduler as Fig.1. According
to weave model, real-time aspect is weavent into the state machine which is used to
express LOTOS specification. Weavent result is expressed by Timed State Machine
as Fig. 2. 
Fig. 1. Automata for Real-Time Constraints