Idle RQ specification

Idle RQ specification: can be combined & used with sequence diagrams

• state transition diagrams    

• extended event-state tables

(1) State Transition Diagrams:

state variables: retain variable information as incoming events are received

• useful for showing correct protocol operations

• space limitations a impractical to show all possible events & conditions

• most state transition diagrams are incomplete specifications

• complete protocol requires many such diagrams

•states are ovals stable point, can be altered by external events

•arcs indicate possible transition between states

•events are occurrences that can cause change in state

- incoming event causing transition (source = LS user, PHYprovider, TIMprovider)

- outgoing events that result from transition (source = LSprovider, PHYuser)

• specific actions : actions internal to state

(2) Extended event-state table: more rigorous method to specify protocol

• basicevent-state table: for any incoming event - only 1 action & 1 next state

• extended: predicates allow alternate actions/next states

for each protocol state (present) and for all possible incoming events

• define outgoing events

• define specific actions

• define alternative actions using predicates

• define new state

• interpreting actions for predicate - assume they are ordered

• lends itself to implementation in SW