State Machine specifications Define behavior using states and transitions between states temp sp/ temp> sp/ turn on heat turn on ac Below At Above setpoint setpoint setpoint temp sp/ emp sp turn off heat turn off ac
State Machine Specifications Define behavior using states and transitions between states temp < sp / temp > sp / setpoint Below setpoint At Above setpoint turn on heat turn on AC temp = sp / temp = sp / turn off heat turn off AC c Copyright Nancy Leveson, Sept. 1999
State Machine Specifications(2 Can easily define time constraints on transitions e.g. telephone switch, must dial 4 digits (internal call) within 10 seconds P offhook Start Timer T(10) Idle Dialtone Await first digit P depress hookswitch 1 thru 8/ Start Timer T(10) Alarm/ Reordertone/Await second digit Alarm T Dia Reordertone o thru 9/- Again Alarm T Await third Reordertone digit Conversing Alarm T o thru 9/- Reordertone Await fourth y o thru 9/ digit Connect
c Copyright Nancy Leveson, Sept. 1999 State Machine Specifications (2) Can easily define time constraints on transitions: e.g. telephone switch, must dial 4 digits (internal call) within 10 seconds P offhook / Start Timer T (10), Dialtone Alarm T / Reordertone Alarm T / Reordertone Alarm T / Reordertone Alarm T / Reordertone Start Timer T (10) P depress hookswitch / Idle Again Dial Await first digit Await second digit Await fourth digit Await third digit Conversing 0 thru 9 / Connect 0 thru 9 / - 0 thru 9 / - 1 thru 8 / - ✁
cruise control turned on initialize cc Cruise Cruise Control on and in Control Standby increase speed commanded Off cruise control Mode send command to throttle turned off to increase at x rate brake depressed Increasing or accelerator depressed Speed discontinue cruise control set point reached / reduce throttle Maintaining Speed read wheel turning rate adjust throttle
cruise control Speed Speed Increasing Maintaining Off Control Cruise Mode Standby and in Control On Cruise or accelerator depressed / cruise control to increase at X rate send command to throttle initialize cc turned on / discontinue brake depressed set point reached / reduce throttle increase speed commanded / cruise control turned off read wheel turning rate / adjust throttle ✂
SpecTRM-RL State explosion prevented by dividing components into parallel state machines Traffic Density Schedule Slot [1...90 LOW Available Average Aircraft Scheduled High Blocked Unknown Unknown Complete state space is the cross product
SpecTRM-RL State explosion prevented by dividing components into parallel state machines. Aircraft Scheduled Available Blocked Unknown Traffic Density Schedule Slot [1...90] High Unknown Low Average Complete state space is the cross product. ✄
SpecTRM-RL (2) Each state can be hierarchically refined Traffic Density Schedule Slot [1...901 LoW Available Average AIRCRAFT SCHEDULED High Aircraft Type Light Unknown Large ETA STA Heavy Unknown BLOCKED Begin Time End Time Unknown
SpecTRM-RL (2) Each state can be hierarchically refined. Traffic Density Schedule Slot [1...90] Available AIRCRAFT SCHEDULED BLOCKED Unknown Aircraft Type STA Begin Time End Time Low Average High Unknown ETA ID Light Large Heavy Unknown ☎