Aspect-Oriented Formal Specification for Real-Time Systems - Advances in Computational Science and Engineering - page 19

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