temperature_sensor.smv

MODULE main

 VAR cpu_temperature: signed word[32];
     sensor_temperature: signed word[32];
       memory: array 0..2 of signed word[32];
       oldest:    {0, 1, 2};
       state:       {0,1,2,3,4,5};
       sleep: signed word[1];

ASSIGN
 init(memory[0]) := 0sd32_0;
 init(memory[1]) := 0sd32_0;
 init(memory[2]) := 0sd32_0;
 init(oldest) := 0;
 init(state) := 0;
 init(sleep) := 0sd1_1;
 init(cpu_temperature) := 0sd32_0; 
 init(sensor_temperature) := 0sd32_0;


next(state) :=
  case state = 0: 1;
       state = 1: 2;
       state = 2: 3;
       state = 3: 4;
       state = 4: 5;
       state = 5: 0;
       TRUE: state;
  esac; 

next(cpu_temperature) :=
  case state = 2 : sensor_temperature;
       state = 4 : cpu_temperature + 0sd32_273;
  TRUE: cpu_temperature;
  esac;

next(sleep) :=
  case state = 1: 0sd1_0;
       state = 3: 0sd1_1;
       TRUE: sleep; 
  esac;

next(oldest ) :=
  case oldest = 2: 0;
       oldest = 0: 1;
       oldest = 1: 2;
       TRUE: oldest;
  esac;


next(memory[0]) :=
  case state = 5 & oldest = 0 : cpu_temperature;
       TRUE: memory[0];
  esac;

next(memory[1]) :=
  case state = 5 & oldest = 1 : cpu_temperature;
       TRUE: memory[1];
  esac;


next(memory[2]) :=
  case state = 5 & oldest = 2 : cpu_temperature;
       TRUE: memory[2];
  esac;



-- Just after the ISR has terminated, the sensor is sleeping.

SPEC AX(state = 5 -> sleep = 0sd1_1);

-- When the sensor is not sleeping, then the ISR is executed.

SPEC AG (sleep = 0sd1_0 -> state != 0) -- state != 0) U (sleep = 0sd1_1)

-- If the ISR is not executed, then the sensor is sleeping.

SPEC AG (state = 0 -> sleep = 0sd1_1);
LTLSPEC (state = 0 | sleep = 0sd1_1) U (state != 0)

-- When the ISR is not executed, then the value of memory at the previous value of oldest is equal to cpu.temperature.

SPEC AG(state = 0 & oldest = 0 -> memory[2] = cpu_temperature);
SPEC AG(state = 0 & oldest = 1 -> memory[0] = cpu_temperature);
SPEC AG(state = 0 & oldest = 2 -> memory[1] = cpu_temperature);

-- Just after the ISR has terminated, then the value of memory at the previous value of oldest is equal to cpu.temperature.

SPEC AX(state = 5 & oldest = 0 -> memory[2] = cpu_temperature);
SPEC AX(state = 5 & oldest = 1 -> memory[0] = cpu_temperature);
SPEC AX(state = 5 & oldest = 2 -> memory[1] = cpu_temperature);

-- When ISR is not executed, then cpu.temperature >= 173.

SPEC AG(state = 0 -> cpu_temperature >= 0sd32_173);

-- When ISR has terminated, then cpu.temperature >= 173.

SPEC AX(state = 5 -> cpu_temperature >= 0sd32_173);

-- oldest is always in the set {0, 1, 2}.

SPEC AG(oldest in {0,1,2});

JUSTICE
  (sensor_temperature >= -0sd32_100) &
  (sensor_temperature <= 0sd32_100);