// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // This case study is due to Mario Trapp and is described in his PhD thesis. // // The program models the control of a light control in a building. // // ************************************************************************** // import LightControl.*; macro LAMPBRIGHTNESS_dimmable = 2; macro LAMPBRIGHTNESS_switchable = 1; macro LAMPBRIGHTNESS_unavailable = 0; macro LAMP_Dimming = 2; macro LAMP_Switching = 1; macro LAMP_Off = 0; macro LIGHTCONTROL_DimmerControl = 3; macro LIGHTCONTROL_IntelligentSwitchControl = 2; macro LIGHTCONTROL_SwitchControl = 1; macro LIGHTCONTROL_Off = 0; macro OCCUPANCY_OccupancyDetection = 4; macro OCCUPANCY_TransponderDetection = 3; macro OCCUPANCY_MotionDetection = 2; macro OCCUPANCY_EntryExitDetection = 1; macro OCCUPANCY_Off = 0; macro ALARMSYSTEM_AlarmLight = 2; macro ALARMSYSTEM_Alarm = 1; macro ALARMSYSTEM_Off = 0; // ================================================================================ // Main Module // ================================================================================ module LightControlSystem( bool ?hasDesiredIlluminance, bool ?hasTransponderID, bool ?hasEntryExit, bool ?hasCurrentIlluminance, bool ?hasMotionDetection, bool ?hasCameraImage, bool ?AlarmNotify, bool ?lightOnOff, bool ?hasDimmerValue, event nat{3} !AlarmCfg, event nat{4} !LightControlCfg, event nat{5} OccupancyMode, event nat{5} !OccupancyCfg, event nat{3} lampBrightness, event nat{3} !LampCfg) { AlarmSystem(AlarmNotify,OccupancyMode,lampBrightness,AlarmCfg); || LightControl(hasDesiredIlluminance,hasCurrentIlluminance,OccupancyMode,lampBrightness,LightControlCfg); || Occupancy(hasMotionDetection,hasCameraImage,hasTransponderID,hasEntryExit,OccupancyMode,OccupancyCfg); || Lamp(hasDimmerValue,lightOnOff,lampBrightness,LampCfg); } // ================================================================================ // Specifications // ================================================================================ satisfies { // ----------------------------------------------------------------------------- // The following specifications state that the services do not get caught in a // state where they are switched off. // ----------------------------------------------------------------------------- ALARMSYSTEM_alive : assert A G ((AlarmCfg==ALARMSYSTEM_Off) -> E F (AlarmCfg!=ALARMSYSTEM_Off)); LIGHTCONTROL_alive : assert A G ((LightControlCfg==LIGHTCONTROL_Off) -> E F (LightControlCfg!=LIGHTCONTROL_Off)); OCCUPANCY_alive : assert A G ((OccupancyCfg==OCCUPANCY_Off) -> E F (OccupancyCfg!=OCCUPANCY_Off)); LAMP_alive : assert A G ((LampCfg==LAMP_Off) -> E F (LampCfg!=LAMP_Off)); // ----------------------------------------------------------------------------- // The next specifications are stronger and assert that every service can reach // all configurations all the time. Hence, there are no deadlocks and no // configuration is unreachable. // ----------------------------------------------------------------------------- ALARMSYSTEM_alive2 : assert A G ((E F (AlarmCfg==ALARMSYSTEM_AlarmLight)) & (E F (AlarmCfg==ALARMSYSTEM_Alarm)) & (E F (AlarmCfg==ALARMSYSTEM_Off)) ); LIGHTCONTROL_alive2 : assert A G ((E F (LightControlCfg==LIGHTCONTROL_DimmerControl)) & (E F (LightControlCfg==LIGHTCONTROL_IntelligentSwitchControl)) & (E F (LightControlCfg==LIGHTCONTROL_SwitchControl)) & (E F (LightControlCfg==LIGHTCONTROL_Off)) ); OCCUPANCY_alive2 : assert A G ((E F (OccupancyCfg==OCCUPANCY_OccupancyDetection)) & (E F (OccupancyCfg==OCCUPANCY_TransponderDetection)) & (E F (OccupancyCfg==OCCUPANCY_MotionDetection)) & (E F (OccupancyCfg==OCCUPANCY_EntryExitDetection)) & (E F (OccupancyCfg==OCCUPANCY_Off)) ); LAMP_alive2 : assert A G ((E F (LampCfg==LAMP_Dimming)) & (E F (LampCfg==LAMP_Switching)) & (E F (LampCfg==LAMP_Off)) ); // ----------------------------------------------------------------------------- // Conversely, each service is always in one of the defined configurations. // Note that unused values of the bitvectors could in principle occur, which // would indicate an erroneous behaviour of the system. // ----------------------------------------------------------------------------- ALARMSYSTEM_reach : assert A G ((AlarmCfg==ALARMSYSTEM_AlarmLight) | (AlarmCfg==ALARMSYSTEM_Alarm) | (AlarmCfg==ALARMSYSTEM_Off) ); LIGHTCONTROL_reach : assert A G ((LightControlCfg==LIGHTCONTROL_DimmerControl) | (LightControlCfg==LIGHTCONTROL_IntelligentSwitchControl) | (LightControlCfg==LIGHTCONTROL_SwitchControl) | (LightControlCfg==LIGHTCONTROL_Off) ); OCCUPANCY_reach : assert A G ((OccupancyCfg==OCCUPANCY_OccupancyDetection) | (OccupancyCfg==OCCUPANCY_TransponderDetection) | (OccupancyCfg==OCCUPANCY_MotionDetection) | (OccupancyCfg==OCCUPANCY_EntryExitDetection) | (OccupancyCfg==OCCUPANCY_Off) ); LAMP_reach : assert A G ((LampCfg==LAMP_Dimming) | (LampCfg==LAMP_Switching) | (LampCfg==LAMP_Off) ); OccupancyMode_reach : assert A G ((OccupancyMode==OCCUPANCY_OccupancyDetection) | (OccupancyMode==OCCUPANCY_TransponderDetection) | (OccupancyMode==OCCUPANCY_MotionDetection) | (OccupancyMode==OCCUPANCY_EntryExitDetection) | (OccupancyMode==OCCUPANCY_Off) ); lampBrightness_reach : assert A G ((lampBrightness==LAMPBRIGHTNESS_dimmable) | (lampBrightness==LAMPBRIGHTNESS_switchable) | (lampBrightness==LAMPBRIGHTNESS_unavailable) ); // ----------------------------------------------------------------------------- // Initially, all configurations are in their "Off" mode. // ----------------------------------------------------------------------------- InitialConfigurations : assert (AlarmCfg==ALARMSYSTEM_Off) & (LightControlCfg==LIGHTCONTROL_Off) & (OccupancyCfg==OCCUPANCY_Off) & (OccupancyMode==OCCUPANCY_Off) & (LampCfg==LAMP_Off) & (lampBrightness==LAMPBRIGHTNESS_unavailable); // ----------------------------------------------------------------------------- // At time step 1, we can reach the following configurations. // These are 2*1*5*1*3*1=30 configurations. // ----------------------------------------------------------------------------- Time1Configurations : assert A X (((AlarmCfg==ALARMSYSTEM_Off) |(AlarmCfg==ALARMSYSTEM_Alarm)) & (LightControlCfg==LIGHTCONTROL_Off) & ((OccupancyCfg==OCCUPANCY_OccupancyDetection) |(OccupancyCfg==OCCUPANCY_TransponderDetection) |(OccupancyCfg==OCCUPANCY_MotionDetection) |(OccupancyCfg==OCCUPANCY_EntryExitDetection) |(OccupancyCfg==OCCUPANCY_Off) ) & (OccupancyMode==OCCUPANCY_Off) & ((LampCfg==LAMP_Dimming) |(LampCfg==LAMP_Switching) |(LampCfg==LAMP_Off) ) & (lampBrightness==LAMPBRIGHTNESS_unavailable) ); // ----------------------------------------------------------------------------- // To reason about the reachable configurations, we verify the following // dependencies: "OccupancyCfg_OccupancyMode" states that "OccupancyMode" is // determined by the previous value of "OccupancyCfg". // ----------------------------------------------------------------------------- OccupancyCfg_OccupancyMode : assert A G (((OccupancyCfg==OCCUPANCY_OccupancyDetection) -> A X (OccupancyMode==OCCUPANCY_OccupancyDetection)) &((OccupancyCfg==OCCUPANCY_TransponderDetection) -> A X (OccupancyMode==OCCUPANCY_TransponderDetection)) &((OccupancyCfg==OCCUPANCY_MotionDetection) -> A X (OccupancyMode==OCCUPANCY_MotionDetection)) &((OccupancyCfg==OCCUPANCY_EntryExitDetection) -> A X (OccupancyMode==OCCUPANCY_EntryExitDetection)) &((OccupancyCfg==OCCUPANCY_Off) -> A X (OccupancyMode==OCCUPANCY_Off)) ); LampCfg_lampBrightness : assert A G (((LampCfg==LAMP_Dimming) -> A X (lampBrightness==LAMPBRIGHTNESS_dimmable)) &((LampCfg==LAMP_Switching) -> A X (lampBrightness==LAMPBRIGHTNESS_switchable)) &((LampCfg==LAMP_Off) -> A X (lampBrightness==LAMPBRIGHTNESS_unavailable)) ); // ----------------------------------------------------------------------------- // If the camera is not available, but the transponder works, the OCCUPANCY // service will be in mode "TransponderDetection". // ----------------------------------------------------------------------------- Lemma : assert A X A G (!hasCameraImage & hasTransponderID -> (OccupancyCfg==OCCUPANCY_TransponderDetection)); }