-------------------------------------------------------------------------------- --- Safety-Critical Java Circus Model in FDR, 2011 written by Frank Zeyda --- -------------------------------------------------------------------------------- --------------- --- Prelude --- --------------- --- Diverging Process --- channel tick --- We use ABORT to model assertion failures in programs. --- ABORT = (let X = tick -> X within X) \ {| tick |} --- We use DEADLOCK_FREE to disregard deadlock after termination. DEADLOCK_FREE = tick -> DEADLOCK_FREE ---------------------- --- Sensor Events --- ---------------------- channel wheel_shaft channel engine_on, engine_off channel brake_pressed, brake_released channel top_gear_engaged, top_gear_disengaged channel activate, deactivate, resume, start_accelerating, stop_accelerating SensorEvents = {| wheel_shaft, engine_on, engine_off, brake_pressed, brake_released, top_gear_engaged, top_gear_disengaged, activate, deactivate, resume, start_accelerating, stop_accelerating |} ----------------------- --- Actuator Events --- ----------------------- VOLTAGE_RANGE = {0..80} channel set_voltage : VOLTAGE_RANGE ActuatorEvents = {| set_voltage |} ----------------------- --- External Events --- ----------------------- ExternalEvents = union(SensorEvents, ActuatorEvents) ----------------- --- Event Ids --- ----------------- datatype EventId = WheelShaftEventId | EngineOnEventId | EngineOffEventId --- BrakePressedEventId | --- BrakeReleasedEventId | --- TopGearEngagedEventId | --- TopGearDisengagedEventId | --- ActivateEventId | --- DeactivateEventId | --- ResumeEventId | --- StartAcceleratingEventId | --- StopAcceleratingEventId ------------------------- --- Process SafeletFW --- ------------------------- SafeletFW = let --- Local Actions --- Setup = setUpCall -> setUpRet -> SKIP Execute = start_sequencer -> done_sequencer -> SKIP TearDown = tearDownCall -> tearDownRet -> SKIP --- Main Action --- within Setup ; Execute ; TearDown ------------------------------ --- Process MainSafeletApp --- ------------------------------ --- Channels --- channel setUpCall, setUpRet channel tearDownCall, tearDownRet MainSafeletAppChan = {| setUpCall, setUpRet, tearDownCall, tearDownRet |} --- Process --- MainSafeletApp = let --- Local Actions --- setUpMeth = setUpCall -> SKIP; setUpRet -> SKIP tearDownMeth = tearDownCall -> SKIP; tearDownRet -> SKIP Methods = let X = setUpMeth ; X within X --- Main Action --- within Methods /\ tearDownMeth --------------------------- --- Process MainSafelet --- --------------------------- MainSafelet = (SafeletFW [| MainSafeletAppChan |] MainSafeletApp) --- \ MainSafeletAppChan ---------------------------------- --- Process MissionSequencerFW --- ---------------------------------- datatype MissionId = MainMissionId | null --- Channels ---- channel start_sequencer, done_sequencer, end_sequencer_app MissionSequencerFWChan = {| start_sequencer, done_sequencer |} --- Process --- MissionSequencerFW = let --- Local Actions --- Start = start_sequencer -> SKIP Execute = let X = getNextMissionRet ? next -> if next != null then start_mission . next -> done_mission . next -> X else SKIP within X Finish = end_mission_fw -> end_sequencer_app -> done_sequencer -> SKIP --- Main Action --- within Start ; Execute ; Finish --------------------------------------- --- Process MainMissionSequencerApp --- --------------------------------------- --- Channels --- channel getNextMissionRet : MissionId MainMissionSequencerAppChan = {| getNextMissionRet, end_sequencer_app |} --- Local Components --- channel mission_done_set, mission_done_get : Bool mission_done_ops = {| mission_done_set, mission_done_get |} mission_done_field(v) = mission_done_set ? v -> mission_done_field(v) [] mission_done_get ! v -> mission_done_field(v) --- Proccess --- MainMissionSequencerApp = let --- Local State --- State = mission_done_field(false) StateChan = mission_done_ops --- Local Actions --- Init = mission_done_set ! false -> SKIP getNextMissionMeth = mission_done_get ? mission_done -> if mission_done == false then mission_done_set ! true -> SKIP ; getNextMissionRet ! MainMissionId -> SKIP else getNextMissionRet ! null -> SKIP --- The following should cause the termination check to fail. --- getNextMissionMeth = --- getNextMissionRet ! MainMissionId -> SKIP Methods = let X = getNextMissionMeth ; X within X --- Main Action --- Main = Init ; Methods MainWithState = (Main [| StateChan |] State) --- \ StateChan within MainWithState /\ end_sequencer_app -> SKIP ------------------------------------ --- Process MainMissionSequencer --- ------------------------------------ MainMissionSequencer = (MissionSequencerFW [| MainMissionSequencerAppChan |] MainMissionSequencerApp) --- \ MainMissionSequencerAppChan ------------------------- --- Process MissionFW --- ------------------------- --- Channels --- channel start_mission, done_mission : MissionId channel add_handler : HandlerId channel activate_handlers, stop_handlers channel end_mission_fw channel end_mission_app : MissionId MissionFWChan = {| start_mission, done_mission, end_mission_fw |} --- Local Components --- channel mission_set, mission_get : MissionId mission_ops = {| mission_set, mission_get |} mission_field(v) = mission_set ? v -> mission_field(v) [] mission_get ! v -> mission_field(v) channel handlers_set, handlers_get : Set(HandlerId) handlers_ops = {| handlers_set, handlers_get |} handlers_field(v) = handlers_set ? v -> handlers_field(v) [] handlers_get ! v -> handlers_field(v) --- Process --- MissionFW = let --- Local State --- State = mission_field(null) ||| handlers_field({}) StateChan = union(mission_ops, handlers_ops) --- Local Actions --- Init = mission_set ! null -> SKIP ; handlers_set ! {} -> SKIP AddHandler(handler) = handlers_get ? handlers -> handlers_set ! union(handlers, {handler}) -> SKIP --- AddHandlers = let X = --- add_handler ? h -> AddHandler(h) ; X within X StartHandlers = handlers_get ? handlers -> (||| h : handlers @ start_handler . h -> SKIP) StopHandlers = handlers_get ? handlers -> (||| h : handlers @ stop_handler . h -> SKIP) DoneHandlers = handlers_get ? handlers -> (||| h : handlers @ done_handler . h -> SKIP) Start = Init ; start_mission ? m -> mission_set ! m -> SKIP --- The following definition of Initialize was flaw: the interrupt may happen --- after synchronisation on add_handler but before the state was accordingly --- updated. Interrupts are dangerous things, good to have FDR to spot it! --- Discuss in Meeting on Mon 7 Feb 2011 --- --- Initialize = --- mission_get ? mission -> --- ((initializeCall . mission -> AddHandlers) --- /\ initializeRet . mission -> SKIP) --- Fixed version of Initialize Initialize = mission_get ? mission -> (initializeCall . mission -> SKIP ; let X = add_handler ? h -> (AddHandler(h) ; X) [] initializeRet . mission -> SKIP within X) Execute = StartHandlers ; activate_handlers -> (DoneHandlers ||| stop_handlers -> StopHandlers) Cleanup = mission_get ? mission -> cleanupCall . mission -> cleanupRet . mission -> SKIP Finish = mission_get ? mission -> end_mission_app . mission -> done_mission . mission -> SKIP --- Main Action --- Main = (let X = Start ; Initialize ; Execute ; Cleanup ; Finish ; X within X) MainWithState = (Main [| StateChan |] State) --- \ StateChan within MainWithState /\ end_mission_fw -> SKIP ------------------------------ --- Process MainMissionApp --- ------------------------------ --- Channels --- channel initializeCall, initializeRet : MissionId channel cleanupCall, cleanupRet : MissionId --- I'm not sure yet what components have to synchronise on channel below. channel missionMemorySizeRet : MissionId . {131072} channel requestTerminationCall, requestTerminationRet : MissionId MainMissionAppChan = {| initializeCall, initializeRet, cleanupCall, cleanupRet, add_handler, stop_handlers, end_mission_app, end_mission_fw |} --- State Components --- channel terminating_set, terminating_get : Bool terminating_ops = {| terminating_set, terminating_get |} terminating_field(v) = terminating_set ? v -> terminating_field(v) [] terminating_get ! v -> terminating_field(v) --- Process --- MainMissionApp = let --- Local State --- State = terminating_field(false) StateChan = terminating_ops --- Local Actions --- Init = terminating_set ! false -> SKIP initializeMeth = initializeCall . MainMissionId -> SKIP ; add_handler ! EngineId -> SKIP ; initializeRet . MainMissionId -> SKIP cleanupMeth = cleanupCall . MainMissionId -> SKIP ; cleanupRet . MainMissionId -> SKIP missionMemorySizeMeth = missionMemorySizeRet . MainMissionId ! 131072 -> SKIP requestTerminationMeth = requestTerminationCall . MainMissionId -> SKIP; (terminating_get ? term -> if term == false then terminating_set ! true -> SKIP ; stop_handlers -> SKIP else SKIP); requestTerminationRet . MainMissionId -> SKIP Methods = let X = ( initializeMeth [] cleanupMeth [] --- missionMemorySizeMeth [] requestTerminationMeth) ; X within X --- Main Action --- --- The Main action has been generalised to support reuse of missions. --- --- Discuss in Meeting on Mon 7 Feb 2011 --- Main = let X = (Init ; Methods) /\ end_mission_app . MainMissionId -> X within X MainWithState = (Main [| StateChan |] State) --- \ StateChan within MainWithState /\ end_mission_fw -> SKIP --------------------------- --- Process MainMission --- --------------------------- MainMission = (MissionFW [| MainMissionAppChan |] MainMissionApp) --- \ MainMissionAppChan ------------------------------- --- Process MainMissionApp2 --- ------------------------------- MainMissionApp2 = let --- Local State --- State = terminating_field(false) StateChan = terminating_ops --- Local Actions --- Init = terminating_set ! false -> SKIP initializeMeth = initializeCall . MainMissionId -> SKIP ; add_handler ! EngineId -> SKIP ; add_handler ! WheelShaftId -> SKIP ; initializeRet . MainMissionId -> SKIP cleanupMeth = cleanupCall . MainMissionId -> SKIP ; cleanupRet . MainMissionId -> SKIP missionMemorySizeMeth = missionMemorySizeRet . MainMissionId ! 131072 -> SKIP requestTerminationMeth = requestTerminationCall . MainMissionId -> SKIP; (terminating_get ? term -> if term == false then terminating_set ! true -> SKIP ; stop_handlers -> SKIP else SKIP); requestTerminationRet . MainMissionId -> SKIP Methods = let X = ( initializeMeth [] cleanupMeth [] --- missionMemorySizeMeth [] requestTerminationMeth) ; X within X --- Main Action --- Main = let X = (Init ; Methods) /\ end_mission_app . MainMissionId -> X within X MainWithState = (Main [| StateChan |] State) --- \ StateChan within MainWithState /\ end_mission_fw -> SKIP ---------------------------- --- Process MainMission2 --- ---------------------------- MainMission2 = (MissionFW [| MainMissionAppChan |] MainMissionApp2) --- \ MainMissionAppChan ---------------------- --- Event Handlers --- ---------------------- --- Handler Ids --- datatype HandlerId = WheelShaftId | EngineId --- BrakeId | --- GearId | --- LeverId | --- ThrottleControllerId | --- SpeedMonitorId --- Channels --- channel start_handler, stop_handler, done_handler : HandlerId --- Declare Handler application channels here --- channel handleAsyncEventCall : HandlerId . EventId channel handleAsyncEventRet : HandlerId --- Channels through which the handlers are controlled by the framework. HandlerFWChan = {| start_handler, stop_handler, done_handler, activate_handlers, end_mission_fw, requestTerminationCall, requestTerminationRet |} --- Channels on which handlers synchronise between themselves. HandlerSyncChan = {| activate_handlers, stop_handlers, end_mission_fw |} --- Local State --- channel active_set, active_get : Bool active_ops = {| active_set, active_get |} active_field(v) = active_set ? v -> active_field(v) [] active_get ! v -> active_field(v) ---------------- --- EngineFW --- ---------------- EngineFW = let --- Local State --- State = active_field(false) StateChan = active_ops --- Local Actions --- Init = active_set ! false -> SKIP StartHandler = start_handler . EngineId -> SKIP ; activate_handlers -> active_set ! true -> SKIP DispatchHandler = let X = ( engine_on -> handleAsyncEventCall . EngineId ! EngineOnEventId -> SKIP ; handleAsyncEventRet . EngineId -> SKIP [] engine_off -> handleAsyncEventCall . EngineId ! EngineOffEventId -> SKIP ; handleAsyncEventRet . EngineId -> SKIP) ; X within X --- I do not think we have to worry about done_handler here. --- Discuss in Meeting on Mon 7 Feb 2011 --- StopHandler = stop_handler . EngineId -> active_set ! false -> SKIP --- Main Action --- Main = let X = Init ; (StartHandler [] activate_handlers -> SKIP) ; active_get ? active -> (if active then (DispatchHandler /\ StopHandler) else SKIP; X) within X MainWithState = (Main [| StateChan |] State) --- \ StateChan within MainWithState /\ end_mission_fw -> SKIP ----------------- --- EngineApp --- ----------------- --- Channels --- --- Because of requestTermination handlers have to interleave. --- However they nevertheless need to synchronise on activate_handlers. EngineAppChan = {| handleAsyncEventCall . EngineId, handleAsyncEventRet . EngineId, stop_handler . EngineId, end_mission_fw |} --- Process --- EngineApp = let --- Local Actions --- Init = SKIP handleAsyncEventMeth = handleAsyncEventCall . EngineId ? event -> (if event == EngineOnEventId then --- Note we cannot raise external events within here as this will deadlock. SKIP else if event == EngineOffEventId then requestTerminationCall . MainMissionId -> SKIP ; requestTerminationRet . MainMissionId -> SKIP else ABORT) ; handleAsyncEventRet . EngineId -> SKIP Methods = let X = (handleAsyncEventMeth; X) [] stop_handler . EngineId -> SKIP within X --- Main Action --- --- I had to remove the interrupt below and replace it by a sequential --- composition in which the Methods action offers the communication for --- stopping the handler. This was necessary because a method call could be --- interrupted by a handler in an awkward moment, that is after its Call --- but before its Ret event. This causes the caller to deadlock. --- A pending problem is that the process may not immediately respond to a --- stop_handler . EngineId communication. A way out of the dilemma could be --- to add a state that records whether the process was stopped. It would, --- however, complicate the model. --- Discuss in Meeting on Mon 7 Feb 2011 --- Main = let X = (Init ; Methods ; done_handler . EngineId -> SKIP) ; X within X within Main /\ end_mission_fw -> SKIP -------------- --- Engine --- -------------- Engine = (EngineFW [| EngineAppChan |] EngineApp) --- \ {| handleAsyncEventCall . EngineId, --- handleAsyncEventRet . EngineId |} -------------------- --- WheelShaftFW --- -------------------- WheelShaftFW = let --- Local State --- State = active_field(false) StateChan = active_ops --- Local Actions --- Init = active_set ! false -> SKIP StartHandler = start_handler . WheelShaftId -> SKIP ; activate_handlers -> active_set ! true -> SKIP DispatchHandler = let X = ( wheel_shaft -> handleAsyncEventCall . WheelShaftId ! WheelShaftEventId -> SKIP ; handleAsyncEventRet . WheelShaftId -> SKIP) ; X within X StopHandler = stop_handler . WheelShaftId -> active_set ! false -> SKIP --- Main Action --- Main = let X = Init ; (StartHandler [] activate_handlers -> SKIP) ; active_get ? active -> (if active then (DispatchHandler /\ StopHandler) else SKIP; X) within X MainWithState = (Main [| StateChan |] State) --- \ StateChan within MainWithState /\ end_mission_fw -> SKIP --------------------- --- WheelShaftApp --- --------------------- --- Channels --- WheelShaftAppChan = {| handleAsyncEventCall . WheelShaftId, handleAsyncEventRet . WheelShaftId, stop_handler . WheelShaftId, end_mission_fw |} --- Process --- WheelShaftApp = let --- Local Actions --- Init = SKIP handleAsyncEventMeth = handleAsyncEventCall . WheelShaftId ? event -> (if event == WheelShaftEventId then engine_off -> SKIP else ABORT) ; handleAsyncEventRet . WheelShaftId -> SKIP Methods = let X = (handleAsyncEventMeth; X) [] stop_handler . WheelShaftId -> SKIP within X --- Main Action --- Main = let X = (Init ; Methods ; done_handler . WheelShaftId -> SKIP) ; X within X within Main /\ end_mission_fw -> SKIP ------------------ --- WheelShaft --- ------------------ WheelShaft = (WheelShaftFW [| WheelShaftAppChan |] WheelShaftApp) --- \ {| handleAsyncEventCall . WheelShaftId, --- handleAsyncEventRet . WheelShaftId |} ---------------------------- --- Composite Processes ---- ---------------------------- MainMissionSequencerComposite = (MainSafelet [| MissionSequencerFWChan |] MainMissionSequencer) --- \ MissionSequencerFWChan MainMissionComposite = MainMissionSequencerComposite [| MissionFWChan |] MainMission --- \ MissionFWChan MainMissionComposite2 = MainMissionSequencerComposite [| MissionFWChan |] MainMission2 --- \ MissionFWChan HandlerSyncChan2 = union(HandlerSyncChan, {| engine_off |}) Handlers = Engine [| HandlerSyncChan2 |] WheelShaft Application = (MainMissionComposite2 [| HandlerFWChan |] Handlers) --- \ HandlerFWChan ---------------------------- --- Assertions and Tests --- ---------------------------- -------------------------------- --- Deadlock Freeness Checks --- -------------------------------- assert (MainSafelet ; DEADLOCK_FREE) :[ deadlock free [FD] ] assert (MainMissionSequencer ; DEADLOCK_FREE) :[ deadlock free [FD] ] assert (MainMissionSequencerComposite ; DEADLOCK_FREE) :[ deadlock free [FD] ] --- MainMissionComposite fails the test because requestTermination may be --- called too soon i.e. before MainMissionApp has been initialised by the --- mission sequencer. assert (MainMission ; DEADLOCK_FREE) :[ deadlock free [FD] ] assert (MainMissionComposite ; DEADLOCK_FREE) :[ deadlock free [FD] ] --- FAILS assert (Handlers ; DEADLOCK_FREE) :[ deadlock free [FD] ] assert (Application ; DEADLOCK_FREE) :[ deadlock free [FD] ] --- FAILS -------------------------- --- Termination Checks --- -------------------------- assert SKIP [FD= (MainSafelet \ Events) assert SKIP [FD= (MainMissionSequencer \ Events) assert SKIP [FD= (MainMissionSequencerComposite \ Events) --- The remaining checks fail because of divergence, caused by events for --- method calls being exposed and continually raised by the environment. assert SKIP [FD= (MainMission \ Events) --- FAILS assert SKIP [FD= (MainMissionComposite \ Events) --- FAILS assert SKIP [FD= (Handlers \ Events) --- FAILS assert SKIP [FD= (Application \ Events) --- FAILS ---------------------------------------------- --- Test Scenario for MainMissionComposite --- ---------------------------------------------- MainMissionCompositeScenario = start_handler . EngineId -> SKIP ; activate_handlers -> SKIP ; requestTerminationCall . MainMissionId -> SKIP ; requestTerminationRet . MainMissionId -> SKIP ; requestTerminationCall . MainMissionId -> SKIP ; requestTerminationRet . MainMissionId -> SKIP ; stop_handler . EngineId -> SKIP ; done_handler . EngineId -> SKIP MainMissionCompositeScenarioChan = {| activate_handlers, start_handler, stop_handler, done_handler, requestTerminationCall, requestTerminationRet |} MainMissionCompositeTest = (MainMissionComposite [| MainMissionCompositeScenarioChan |] MainMissionCompositeScenario) --- \ MainMissionCompositeScenarioChan assert (MainMissionCompositeTest ; DEADLOCK_FREE) :[ deadlock free [FD] ] assert SKIP [FD= (MainMissionCompositeTest \ Events) -------------------------------- --- Test Scenario for Engine --- -------------------------------- EngineScenario = start_handler . EngineId -> SKIP ; activate_handlers -> SKIP ; engine_on -> SKIP; engine_off -> SKIP; stop_handler . EngineId -> SKIP ; done_handler . EngineId -> SKIP ; end_mission_fw -> SKIP EngineScenarioChan = union( {| start_handler, stop_handler, done_handler, activate_handlers, end_mission_fw |}, ExternalEvents) EngineTest = (Engine [| EngineScenarioChan |] EngineScenario) assert (EngineTest ; DEADLOCK_FREE) :[ deadlock free [FD] ] assert SKIP [FD= (EngineTest \ Events) ------------------------------------- --- Test Scenario for Application --- ------------------------------------- ApplicationScenario1 = engine_on -> SKIP ; engine_off -> SKIP --- engine_off -> SKIP ApplicationScenario2 = wheel_shaft -> SKIP ; engine_off -> SKIP ApplicationTest = (Application [| ExternalEvents |] ApplicationScenario2) --- \ ExternalEvents assert (ApplicationTest ; DEADLOCK_FREE) :[ deadlock free [FD] ] assert SKIP [FD= (ApplicationTest \ Events)