Information Technology Reference
In-Depth Information
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. [30]
Fig. 1. Automata for Real-Time Constraints
Search WWH ::

Custom Search