Automating a labor-intensive process
Doron is the founder of Time Rover and author of Temporal Rover and DBRover. He can be contacted at http://www.time-rover.com/.
Software verification has been a concern for more than 20 years. However, recent security flaws in mainstream products (Internet Explorer, for instance) and software failures (such as the French Ariane 5 rocket fiasco) have brought renewed focus on the topic.
Runtime monitoring is one lightweight formal software verification technique. However, this technique is also used for nonverification purposes, including temporal business rule checking and temporal rules in expert systems. In this article, I examine the concept of runtime monitoring, focusing on its application to robust system verification.
Unlike conventional testing methods, which are human intensive, slow, expensive, and error prone, formal methods make automated computer-based verification possible. However, most formal methods (model checking and theorem proving, for instance) suffer from limited acceptance because of factors ranging from computational complexity to the high level of mathematical skills needed to be used effectively. Runtime monitoring, which is based on formal specifications, is similar to conventional testing in that it depends on actual system execution, either in test mode or in the field. The benefits of runtime monitoring over formal methods such as model checking are:
- Scalability. Runtime monitoring scales well in that they can be applied to large systems using existing programming languages such as C, C++, and Java.
- Expressiveness. Runtime monitoring techniques can be used to check properties that include real-time constraints and time-series constraints
Still, the main benefit of runtime monitoring over conventional testing is that it can be automated via executable specifications. In addition, runtime monitoring can be used beyond the testing phase to monitor the system and also to recover from runtime-specification errors.
Runtime Monitoring Using Executable Specifications
A formal specification is a description of what the system should and should not do, using a language that computers can understand and ultimately execute (see the accompanying text box entitled "Formal Specifications"). Runtime monitoring can be thought of as the process of executing formal specifications as a real computer program. Runtime monitoring primarily focuses on the execution and evaluation of a particularly difficult aspect of formal specification—namely, ordering and temporal relationships between events, conditions, and other artifacts of computations. Of particular interest is on-line runtime monitoring, where monitoring is performed for very long and potentially neverending computations.
Consider, for example, an infusion pump control. The infusion pump consists of six conditions: (infusion) begin, (infusion) end, keyPressed, valveOpen (where valveClosed = !valveOpen), pumpOn (where pumpClosed = !pumpOn), and alarm.
The pump operates (pumpOn is True) in intervals between a begin and end that coincides with the valve being closed for more than 10 seconds. For every such interval, a human-induced keyPressed must be repeatedly sensed within two-minute intervals; otherwise, an alarm sounds within 10 seconds. Following an alarm, a subsequent keyPressed event terminates the alarm.
Listing One is Java code for an infusion pump controller within a simulation wrapper. In addition, Listing One includes three embedded temporal logic assertions written as source-code comments. They correspond to the following natural language assertions:
- Assertion MUST_SHUT_PUMP. An end sensed after 10 or more continuous seconds of valveClosed must force pump off.
- Assertion NEVER_SHUT_PUMP_TOO _SOON. Never shut pump off unless valve is closed for at least 10 continuous seconds.
- Assertion NO_KEYPRESSED_FORCES _ALARM. While pump is on, if keyPressed does not occur within two minutes, then alarm should sound within 10 seconds afterwards.
The two primary techniques for monitoring these requirements during the execution of the infusion pump software are in-process monitoring and remote monitoring.
In-process monitoring resembles conventional programming language assertions such as those in C, C++, or Java. Unlike conventional assertions, however, in-process runtime monitoring supports the verifications of complex requirements that assert over time and order, as with the three infusion pump assertions. In fact, conventional assertions are comparable to temporal logic assertions where the only allowable temporal operator is the Always operator. The infusion pump temporal assertions in Listing One are preprocessed for in-process monitoring using a commercial temporal logic code generator (in this case, Temporal Rover, developed by my company), which replaces the comment-based temporal assertions of Listing One with executable Java, C, C++, or Matlab code. It is this generated code that performs runtime, in-process monitoring for the infusion pump controller.
Listings Two and Three are excerpts of the infusion pump simulation report, including runtime-monitoring printouts (the complete report is available electronically; see "Resource Center," page 5). In this example, runtime monitoring uncovered the following bugs:
- The infusion pump controller, after two minutes of no key-press, goes into an alarm-generation mode where it misses the detection of a shutdown (end) command. Uncovered by Test #1 and assertion MUST_SHUT_PUMP.
- The infusion pump controller, while counting 10 seconds of valveClosed, misses the event valveOpen and loses synchronization with the state of the valve. Consequently, it permits pump shutoff, although the valve has not been closed for 10 continuous seconds. Uncovered by Test #2 and assertion NEVER_SHUT_PUMP_TOO_SOON.
With remote monitoring, special probing code (automatically generated by the runtime monitoring tool) is used instead of the temporal assertion comments. These probes access changes to basic Boolean events and conditions of interest, such as keyPressed, alarm, and valveOpen, and feed the runtime monitor with the information it needs to execute the formal specifications. With remote monitoring, the formal specification rules are executed remotely within the remote monitor.
Advantages of remote monitoring over in-process monitoring include: Remote monitors have lower impact on the real-time performance of target systems, they have almost no memory footprint on the target system, and they serve as a central repository of requirements and assertions.
Runtime monitoring is applicable early in the design process using prototyping tools such as Matlab and modeling methodologies such as the UML. Figure 1, for example, is a UML statechart for the infusion pump with assertions embedded in states. It is possible then, using commercial statechart tools, to invoke a runtime monitoring code generator for these assertions during statechart code generation, thereby generating statechart code that is armor plated with executable temporal assertions.
Following early phase prototyping, runtime monitoring is also applicable on the cross-platform simulation and testing level and eventually on an embedded target for purposes of monitoring in the field. The Jet Propulsion Lab, for instance, has applied runtime monitoring on a cross-platform simulator to verify flight code for the Deep Impact project (see "Applying Runtime Monitoring to the Deep-Impact Fault Protection Engine," by D. Drusinsky and G. Watney, 28th IEEE/NASA Software Engineering Workshop, 2003).
Considering the garbage-in/garbage-out effect that poor specifications (formal and informal) have on the quality of software, it is desirable to perform thorough simulations of formal specification requirements. Some commercial runtime monitors provide built-in temporal rule simulators. Figures 2(a) and 2(b) illustrate the simulation of the NO_KEYPRESSED_FORCES_ALARM assertion under two scenarios.
Simulation is also necessary for the exchange of formal requirements within development teams or for purposes of distributed research and development, where teams need to share both the formal requirements and all mutually acceptable simulation scenarios for those requirements.
DDJ
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;
}
}
Back to articleListing 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 ********
Back to articleListing 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
Back to article
