Run-Time Monitoring & Software Verification
by Doron Drusinsky

Listing One
import java.io.*;
// a little simulation and assertion wrapper for the InfusionPump
public class InfusionPumpMain  {
    static Sim sim;
    public static void main(String argv[]) {
       sim = new Sim();
       sim.run();
    }
}
//==========================================================
class Sim {
   boolean begin = false;
   Alarm alarm = new Alarm(false);
   boolean end = false;
   boolean keyPressed = false;
   boolean valveOpen = false;
   int globalTime;
   InfusionPump ip;
   //A keyword required for the TemporalRover code generator
   //TRDecl
   void resetAssertions() {
     //A keyword required for the TemporalRover code generator
      //TRReset
   }
    void run() {
      globalTime = 0;
      //* Test 1: begin.valveClosed(x 11).valveOpen(110).valveClosed(x 11).end
      //             Pump should shut off
      System.out.println("************ Test1 ********");
      globalTime = 0;
      ip = new InfusionPump();
      resetAssertions();
      begin = true;
      fireInfusionPump(ip); // time= 0
      fireInfusionPump(ip); // no interesting event, time= 1
      fireInfusionPump(ip); // no interesting event, time= 2
      fireInfusionPump(ip); // no interesting event, time= 3
      fireInfusionPump(ip); // no interesting event, time= 4
      fireInfusionPump(ip); // no interesting event, time= 5
      fireInfusionPump(ip); // no interesting event, time= 6
      fireInfusionPump(ip); // no interesting event, time= 7
      fireInfusionPump(ip); // no interesting event, time= 8
      fireInfusionPump(ip); // no interesting event, time= 9
      fireInfusionPump(ip); // no interesting event, time= 10
      fireInfusionPump(ip); // no interesting event, time= 11

      valveOpen = true;
      fireInfusionPump(ip); // time = 12
      valveOpen = true;
      fireInfusionPump(ip);
      ... 110 cycles with valveOpen = true;
      // time = 122
      fireInfusionPump(ip
      ... 11 cycles with valveOpen = false;
      end = true;
      fireInfusionPump(ip);
      fireInfusionPump(ip); // pump should be off!
      System.out.println("************ End Test1 ********");
      //**** Test 1 end
      //* Test 2: begin.valveClosed(x 2).valveOpen(x 6).valveClosed(x 5).end
      //    Pump should NOT shut off (no continuous 10 seconds of valveClosed)
      System.out.println("************ Test2 ********");
      globalTime = 0;
      ip = new InfusionPump();
      resetAssertions();
      begin = true;
      fireInfusionPump(ip); // time= 0
      fireInfusionPump(ip); // no interesting event, time= 1
      fireInfusionPump(ip); // no interesting event, time= 2
      valveOpen = true;
      fireInfusionPump(ip); // time =3
      valveOpen = true;
      fireInfusionPump(ip); // time= 4
      valveOpen = true;
      fireInfusionPump(ip); // time= 5
      valveOpen = true;
      fireInfusionPump(ip); // time= 6
      valveOpen = true;
      fireInfusionPump(ip); // time= 7
      valveOpen = true;
      fireInfusionPump(ip); // time= 8

      // now valveClosed = true;
      fireInfusionPump(ip); // time= 9
      fireInfusionPump(ip); // time= 10
      fireInfusionPump(ip); // time= 11
      fireInfusionPump(ip); // time= 12
      fireInfusionPump(ip); // time= 13

      end = true;
      fireInfusionPump(ip); // time= 14, pump should NOT shut down
      System.out.println("************ End Test2 ********");
      //**** Test 2 end
    }
    void fireInfusionPump(InfusionPump ip) {
      System.out.println("");
      System.out.print("*** Infusion Pump: time=" + (globalTime++));
      System.out.print("; inputs: begin="+begin + ", end="+end);
      System.out.println(",keyPressed="+keyPressed + ",valveOpen="+valveOpen);
      boolean valveClosed = !valveOpen;
      ip.fire(begin, alarm, end, keyPressed, valveOpen);
      /*********************** Assertions ***********************************/
      /* TRBegin
         //Global assertions; assertions for the entire infusion pump.
         //     The syntax used is the TemporalRover syntax.
         // Assertion "MUST_SHUT_PUMP": valve closed for more than 10
         // seconds followed by an end event must force pump off
         TRAssert {
           Always ( {valveClosed} ->
             Not ({valveClosed} Until_>=10_ ({end} And Not Next
{ip.isPumpOff()}))
                  )} => // now come the actions
          {System.out.println("Assertion MUST_SHUT_PUMP: SUCCESS");$
                   // custom action,  performed whenever assertion succeeds
           System.out.println("Assertion MUST_SHUT_PUMP: FAIL");$$
                    // custom action, performed whenever assertion fails
           System.out.println("Assertion MUST_SHUT_PUMP: DONE");}
               // custom action, performed whenever assertion result becomes
immutable
         // Assertion "NEVER_SHUT_PUMP_TOO_SOON": never shut pump off unless
valve is closed
         // for at least ten continuous seconds
         TRAssert {
           Next Always ( Not ({valveClosed} And Previous{valveOpen} And
                                             Eventually_<10_{ip.isPumpOff()}) )}
                  => // now come the actions
          {System.out.println("Assertion NEVER_SHUT_PUMP_TOO_SOON: SUCCESS");$
           System.out.println("Assertion NEVER_SHUT_PUMP_TOO_SOON: FAIL");$$
           System.out.println("Assertion NEVER_SHUT_PUMP_TOO_SOON: DONE");}
         // Assertion "NO_KEYPRESSED_FORCES_ALARM": while in pump is on, if
         //   keyPressed does not occur within two minutes
         //   then alarm should sound within 10 seconds afterwards
         TRAssert {
           Always ( {ip.isPumpOn()} ->
                    ((Always_<120_ {!keyPressed && ip.isPumpOn()}) ->
                                (Eventually_[120,130]_{alarm.booleanValue()}) )
                  )} => // now come the actions
          {System.out.println("Assertion NO_KEYPRESSED_FORCES_ALARM: SUCCESS");$
           System.out.println("Assertion NO_KEYPRESSED_FORCES_ALARM: FAIL");$$
           System.out.println("Assertion NO_KEYPRESSED_FORCES_ALARM: DONE");}
     TREnd*/
      /*********************** End Assertions ******************************/
      begin = false;
      end = false;
      keyPressed = false;
      valveOpen = false;
      waitOneSec(); // firing of infusion pump controller at a 1Hz frequency
    }
    private void waitOneSec() {
      Thread t = new Thread();
      try {
        t.sleep(1000);
      } catch (java.lang.InterruptedException e) {
        System.err.println(e);
        return;
      }
    }
} /* end class */
//=================================================
class Timer extends Thread {
  private int m_nSecCounter;
  private boolean m_isTimeout;
  Timer(int nSec) {
    m_nSecCounter = nSec;
    m_isTimeout = false;
  }
  public void run() {
    try {
      sleep(m_nSecCounter*1000);
    } catch (java.lang.InterruptedException e) {
      System.err.println(e);
      return;
    }
    m_isTimeout = true;
  }
  boolean isTimeout() {
    return m_isTimeout;
  }
} /* end class */
//===============================================
class InfusionPump {
   public static final int TR_CONC_LEVEL_INFUSIONPUMP = 3;
   private static final int DONT_CARE = 7;
   private static final int DUMMY = 6;
   private static final int DUMMYNONREST = 0;
   public static final int St_InfusionPump_Alarm_Necessary = 0;// mapped to
PS[0]
   public static final int St_InfusionPump_Alarm = 1;// mapped to PS[0]
   public static final int St_InfusionPump_OPN = 3;// mapped to PS[0]
   public static final int St_InfusionPump_CLS = 4;// mapped to PS[0]
   public static final int St_InfusionPump_PumpOff = 5;// mapped to PS[0]
   public static final int St_InfusionPump_WaitForKeyPressed = 0;// mapped to
PS[1]
   private int[] PS = new int[TR_CONC_LEVEL_INFUSIONPUMP];
   private int[] NS = new int[TR_CONC_LEVEL_INFUSIONPUMP];
   private Timer timer_10;
   private Timer timer_120;
   // constructor
   InfusionPump()  {
      PS[0] = St_InfusionPump_PumpOff;
      NS[0] = St_InfusionPump_PumpOff;
      PS[1] = DUMMY;
      NS[1] = DUMMY;
      PS[2] = DUMMY;
      NS[2] = DUMMY;
   }
   /* @param inputs: begin, end, keyPressed, valveOpen; output: alarm */
   void fire(boolean begin, Alarm alarm, boolean end, boolean keyPressed,
boolean valveOpen) {
      int TR_i;
      for( TR_i=0; TR_i<TR_CONC_LEVEL_INFUSIONPUMP; TR_i++ ) {
               NS[TR_i] = DONT_CARE;
      }
      if(PS[0] == St_InfusionPump_PumpOff)  {
            alarm.set(false);
            if(begin)    {
               if((NS[0] == DONT_CARE) && (NS[1] == DONT_CARE) && (NS[2] ==
DONT_CARE))   {
                  System.out.println("   ---> Pump ON! waiting for operator
key-press ***");
                  NS[0] = St_InfusionPump_CLS;
                  NS[1] = St_InfusionPump_WaitForKeyPressed;
                  NS[2] = 0;
                  tmCount(10);
                  tmCount(120);
               }
            }
      }
      if(PS[1] == St_InfusionPump_WaitForKeyPressed)  {
            if(tm(120))  {
               if((NS[0] == DONT_CARE) && (NS[1] == DONT_CARE) && (NS[2] ==
DONT_CARE))     {
                  System.out.println("   ---> 2 minutes elapsed without operator
key-press;
                                                                       generate
alarm ***");
                  NS[0] = St_InfusionPump_Alarm_Necessary;
                  NS[1] = DUMMY;
                  NS[2] = DUMMY;
               }
            }
      }
      if(PS[0] == St_InfusionPump_Alarm_Necessary)   {
               System.out.println("     ---> alarm ON***");
               alarm.set(true);
               if((NS[0] == DONT_CARE) && (NS[1] == DONT_CARE) && (NS[2] ==
DONT_CARE))     {
                  NS[0] = St_InfusionPump_Alarm;
                  NS[1] = DUMMY;
                  NS[2] = DUMMY;
               }
      }
      if(PS[0] == 2) {
            if(end)  {
               if((NS[0] == DONT_CARE) && (NS[1] == DONT_CARE) && (NS[2] ==
DONT_CARE))     {
                  System.out.println("     ---> Pump OFF! ***");
                  NS[0] = St_InfusionPump_PumpOff;
                  NS[1] = DUMMY;
                  NS[2] = DUMMY;
                  alarm.set(false);
               }
            }
      }
      if(PS[0] == St_InfusionPump_Alarm)  {
            if(keyPressed)  {
               if((NS[0] == DONT_CARE) && (NS[1] == DONT_CARE) && (NS[2] ==
DONT_CARE))    {
                  System.out.println("  ---> alarm OFF, waiting for operator
key-press***");
                  alarm.set(false);
                  NS[0] = St_InfusionPump_CLS;
                  NS[1] = St_InfusionPump_WaitForKeyPressed;
                  NS[2] = 0;
                  tmCount(10);
                  tmCount(120);
               }
            }
      }
      if(PS[0] == St_InfusionPump_OPN)  {
            if(!valveOpen)  {
               if(NS[0] == DONT_CARE)    {
                  System.out.println("     ---> valve is closed ***");
                  NS[0] = St_InfusionPump_CLS;
                  tmCount(10);
               }
            }
      }
      if(PS[1] == St_InfusionPump_WaitForKeyPressed)  {
            if(keyPressed)   {
               if(NS[1] == DONT_CARE)    {
                  System.out.println("     ---> detected key-press ***");
                  NS[1] = St_InfusionPump_WaitForKeyPressed;
                  tmCount(120);
               }
            }
      }
      if(PS[0] == 2)   {
            if(valveOpen)   {
               if(NS[0] == DONT_CARE)    {
                  System.out.println("     ---> valve is open ***");
                  NS[0] = St_InfusionPump_OPN;
               }
            }
      }
      if(PS[0] == St_InfusionPump_CLS)   {
            if(tm(10))    {
               System.out.println(" ---> done counting 10 seconds of
valve-closed before
                                                                    pump shut
down ***");
               if(NS[0] == DONT_CARE)    {
                  NS[0] = 2;
               }
            }
      }
      /* assigning next state to present state */
      for( TR_i=0; TR_i<TR_CONC_LEVEL_INFUSIONPUMP; TR_i++ ) {
               if(NS[TR_i] != DONT_CARE) {
                  PS[TR_i] = NS[TR_i];
               }
      }

   }
   private boolean tm(int nSec) {
     boolean bRet;
     switch(nSec) {
       case 10: bRet = timer_10.isTimeout();
         break;
       case 120: bRet = timer_120.isTimeout();
         break;
       default: bRet = false;
     }
     return bRet;
   }
   private void tmCount(int nSec) {
     switch(nSec) {
       case 10:
         timer_10 = new Timer(10);
         timer_10.start();
         break;
       case 120:
         timer_120 = new Timer(120);
         timer_120.start();
         break;
     }
   }
   boolean isPumpOff() {
     return PS[0] == St_InfusionPump_PumpOff;
   }
   boolean isPumpOn() {
     return PS[0] != St_InfusionPump_PumpOff;
   }
   boolean inState_WaitForKeyPressed() {
     return PS[1] == St_InfusionPump_WaitForKeyPressed;
   }
} /* end class */
//===================================================
class Alarm {
  private boolean m_value;
  Alarm(boolean val) {
    m_value = val;
  }
  void set(boolean newVal) {
    m_value = newVal;
  }
  boolean booleanValue() {
    return m_value;
  }
}


Listing Two
*** Infusion Pump: time=0; inputs: begin=true,
***     end=false, keyPressed=false, valveOpen=false
     ---> Pump ON! waiting for operator key-press ***
Assertion MUST_SHUT_PUMP: FAIL
Assertion NEVER_SHUT_PUMP_TOO_SOON: FAIL
Assertion NO_KEYPRESSED_FORCES_ALARM: FAIL

*** Infusion Pump: time=1; inputs: begin=false,
***     end=false, keyPressed=false, valveOpen=false
Assertion MUST_SHUT_PUMP: FAIL
Assertion NEVER_SHUT_PUMP_TOO_SOON: SUCCESS
Assertion NO_KEYPRESSED_FORCES_ALARM: FAIL
  .
  .
  .
*** Infusion Pump: time=133; inputs: begin=false,
***       end=true, keyPressed=false, valveOpen=false
Assertion MUST_SHUT_PUMP: FAIL
Assertion NEVER_SHUT_PUMP_TOO_SOON: SUCCESS
Assertion NO_KEYPRESSED_FORCES_ALARM: FAIL

*** Infusion Pump: time=134; inputs: begin=false,
***                  end=false, keyPressed=false, valveOpen=false
Assertion MUST_SHUT_PUMP: FAIL
Assertion MUST_SHUT_PUMP: DONE                  <--- bug #1 caught
Assertion NEVER_SHUT_PUMP_TOO_SOON: SUCCESS
Assertion NO_KEYPRESSED_FORCES_ALARM: FAIL
************ End Test1 ********

Listing Three
*** Infusion Pump: time=10; inputs: begin=false,
***     end=false, keyPressed=false, valveOpen=false
     ---> done counting 10 seconds of valve-closed before pump shut down ***
Assertion MUST_SHUT_PUMP: FAIL
Assertion NEVER_SHUT_PUMP_TOO_SOON: SUCCESS
Assertion NO_KEYPRESSED_FORCES_ALARM: FAIL

*** Infusion Pump: time=11; inputs: begin=false,
***     end=false, keyPressed=false, valveOpen=false
Assertion MUST_SHUT_PUMP: FAIL
Assertion NEVER_SHUT_PUMP_TOO_SOON: SUCCESS
Assertion NO_KEYPRESSED_FORCES_ALARM: FAIL

*** Infusion Pump: time=12; inputs: begin=false,
***     end=false, keyPressed=false, valveOpen=false
Assertion MUST_SHUT_PUMP: FAIL
Assertion NEVER_SHUT_PUMP_TOO_SOON: SUCCESS
Assertion NO_KEYPRESSED_FORCES_ALARM: FAIL

*** Infusion Pump: time=13; inputs: begin=false,
***     end=false, keyPressed=false, valveOpen=false
Assertion MUST_SHUT_PUMP: FAIL
Assertion NEVER_SHUT_PUMP_TOO_SOON: SUCCESS
Assertion NO_KEYPRESSED_FORCES_ALARM: FAIL

*** Infusion Pump: time=14; inputs: begin=false,
***     end=true, keyPressed=false, valveOpen=false
     ---> Pump OFF! ***
Assertion MUST_SHUT_PUMP: FAIL
Assertion NEVER_SHUT_PUMP_TOO_SOON: FAIL
Assertion NEVER_SHUT_PUMP_TOO_SOON: DONE          <--- bug #2 caught
Assertion NO_KEYPRESSED_FORCES_ALARM: SUCCESS






