Transcript PACEMAKER Project Overall Plan (v0.5)

Toward Safety-Assured Development
of Real-Time Software
November 5, 2011
Eunkyoung Jee, Oleg Sokolsky, Insup Lee
PRECISE center, Department of Computer and Information Science
University of Pennsylvania
Outline
 Introduction
 Case Study: Pacemaker
 A Safety-Assured Development Approach for RTS
 Formal Modeling and Verification
 Implementation and Timing Analysis
 Property Preservation
 Limitations and Possibilities
 Conclusion and Future Work
2
Introduction
 Guaranteeing timing properties is crucial
for real-time safety critical systems
 We can have a formally verified model
 How can we implement time-guaranteed
real-time software from a verified
model?
 Present a safety-assured development
approach for real-time software
 Model-driven development + timing analysis
 Pacemaker case study
3
Case Study: Pacemaker
 Electronic device implanted in the
body to regulate the heart beat
 A life-critical real-time embedded system
 The Pacemaker Grand Challenge
 The first certification challenge problem
issued by the Software Certification
Consortium (SCC)
 Boston Scientific has released into the
public domain the system specification
for a previous generation pacemaker
4
img src: http://www.odec.ca/projects/2007/
torr7m2/images/pacemaker.gif
Pacemaker Timing
 Two basic functions
 Pace
 Sense intrinsic rhythm and inhibit
 Fundamental timing cycles of VVI mode (simplest mode)
LRI
LRI
HRI (> LRI)
VRP
VRP
VRP
5
VRP
• LRI: Lower Rate Interval (e.g., 1000ms)
• HRI: Hysteresis Rate Interval (e.g., 1200ms)
• VRP: Ventricular Refractory Period (e.g., 320ms)
A Safety-Assured Development
Software
life cycle
Development
process
Requirement
analysis
(1)
System
spec.
Design
Timed
automata
model
Implementation
(3)
C code
synthesis
compile
(4)
(2)
Verification
and
validation
process
Integration
Measurement
based
timing analysis
Model checking
(with UPPAAL)
(5)
Re-checking
with ∆
6
Manual
Semi-automatic
Automatic
Formal Modeling in UPPAAL
Pacemaker on VVI mode
Heart
Ventricular
controller
7
Formal Verification
 Model checking using UPPAAL
 Covered properties
 PropLRI: Hysteresis pacing is deactivated  a ventricular pace or sense
should be no later than LRI
 A[] (!Ventricle.hpenable imply Ventricle.x <= Ventricle.LRI)
 PropHRI: Hysteresis pacing is activated  a ventricular pace or sense
should be no later than HRI
 A[] (Ventricle.hpenable imply Ventricle.x <= Ventricle.HRI)
 PropVRP: Sensing cannot occur before VRP ends
 A[] ((Ventricle.WaitRI && Ventricle.started) imply Ventricle.x >=
Ventricle.VRP)
 Deadlock freeness
 A[] (not deadlock)
All these properties were satisfied on the model
We assume that users capture all the important
properties correctly.
8
Code Synthesis & Timing Analysis
(1)
Timed
automata
model
Produce C code from the timed
automata model systematically
(3)
C code
synthesis
Check whether the timing properties are
satisfied in the code (by testing)
For each of violating properties,
measure how much deviations occur
 Find a timing tolerance ∆
(4)
(2)
Measurement
based
timing analysis
Model checking
(with UPPAAL)
(5)
Modify the code and the model with ∆
Re-checking
with ∆
Check again that the model and the
code satisfy all the properties within ∆
9
Code Synthesis
 Code generated by the TIMES tool
 Amnell et al., Code synthesis for timed automata, Nordic
Journal of Computing, 9(4), pp. 269-300, 2003
 Generated code ported to a different platform
 Replacing system calls does not change functional behavior
10
Property Checking in Code by Testing
 Inserted “if-then-else” checking statements inside the loop for
the properties which should be satisfied all the times
 Performed simulation-based black box testing
 Findings
 Code execution time harms property preservation
 Characteristics of timing properties matters
 clock_var  limit (e.g. PropVRP) are guaranteed
 clock_var  limit (e.g. PropLRI, PropHRI) are not guaranteed
 Time deviations were bounded in the tested scenarios (E.g.,  1ms)
11
Timing Tolerance ∆
 Modify the code and the model referring to the violated
properties to keep the properties transferred from the model in
the code
 Strategy for converting the violated properties to the satisfied
ones
Find a timing tolerance ∆ by measuring deviations from
the desired time
Make the desired events happen no later than the
predetermined time T by evaluating guard at ∆ time units
earlier than T, while not violating all other properties
12
Re-checking with Timing Tolerance ∆
Change the code
minimally
#define DELTA (some value)
∆ was set as 2ms in our case
…
bool eval_guard(int trn) {
Relax guard in the code with ∆
switch(trn) {
case 0: return (Heart_flag>0);
case 2: return (rdClock(Ventricle_x)>=Ventricle_RI - DELTA;
case 4: return (rdClock(Ventricle_x)>=Ventricle_VRP);
...
}
Make the corresponding changes
in the model
Check whether the
changes affect
other properties
x >= RI – DELTA Relax guard in the model with ∆
Verified all the properties again
 Confirmed that all the properties were still
preserved within the tolerance bound
13
Limitations and Possibilities
 Type of timing properties
 Combinations of complex timing properties need to be considered
 Instrumentation overhead
 Time overhead from instrumentation may cause the code to fail in satisfying timing
properties, although not in our example
 Existing techniques for improving the performance and accuracy of time profilers
based on code instrumentation can be applied to our approach
 Timing analysis on C code
 Simple measurement technique to find timing tolerances can be replaced by WCET
techniques
 Generalization
 Other modeling languages, verification tools, code synthesis techniques, and timing
analysis techniques can be used as long as they satisfy minimum requirements
 Scalability
 Semi-automatic code synthesis and manual modifications to the model could be
automated by development of proper tools
14
Conclusion & Future Work
 Proposed a safety-assured development approach for real-
time software
 Combined the model-driven development methodology and the
measurement-based timing analysis
 Suggested a way to achieve property preservation within the timing
tolerance in the code
 Demonstrated the proposed approach using pacemaker software
 Future Work
 Complement measurement-based timing analysis with formal analysis
(e.g. WCET)
 Complement testing by code level verification
15
Questions?
16
References
 [AFP+03] T. Amnell, E. Fersman, P. Pettersson, W. Yi, and H. Sun, “Code
synthesis for timed automata,” Nordic J. of Computing, vol. 9, no. 4, pp.
269–300, 2002.
 [DDR04] M. de Wulf, L. Doyen, and J.-F. Raskin, “Systematic implementation
of real-time models,” in FM, ser. Lecture Notes in Computer Science, J.
Fitzgerald, I. J. Hayes, and A. Tarlecki, Eds., vol. 3582. Springer, 2005, pp.
139–156.
 [AT05] K. Altisen and S. Tripakis, “Implementation of timed automata: an
issue of semantics or modeling,” in In Proc. 3rd Int. Conf. Formal Modelling
and Analysis of Timed Systems (FORMATS05), Lecture Notes in Computer
Science. Springer, 2005, pp. 273–288.
17
Backup Slides
Property Checking in Code
 Inserted “if-then-else” checking statements into the end of the
loop for each “A[] P” safety property
…
for each trn do
if (trn is active) and (eval_guard(trn))
if (there is synchronization)
if (compl_trn exists) and (eval_guard(compl_trn))
read test_clock;
Timer value used in
/* for property checking */
checking is a value after
update variables of both trn and compl_trn;
take both trn and comp_trn to new states;
guard evaluation
check properties and print results;
followed by check_synch
/* for property checking */
set trn to -1; /* check all outgoing transitions again */
and before taking to
end if
next state
else /* no synchronization */
update variables of trn;
take the transition trn to new state;
set trn to -1;
end if
end if
end if
end for
…
19
Timer Checking Point
void check_trans() {
…
for(trn=0; trn<NB_TRANS; trn++) {
if( trans[trn].active ) {
if( eval_guard(trn) ) {
if( trans[trn].sync > -1 ) {
if( (compl_trn =
check_synch( trans[trn].sync )) ) {
/********** verification *****************/
if(Ventricle_hpenable == false){
if(clock_aa <= Ventricle_LRI){
putrsUSART(" (TL: ");
putsUSART(itoa(clock_aa, time));
putrsUSART(")\n");
}
else{
/*store current time for verification*/
clock_aa = rdClock(Ventricle_x);
if( IS_SEND(trans[trn].sync) ) {
assign( trn );
assign( compl_trn );
}
else {
assign( compl_trn );
assign( trn );
}
clear_and_set( trn );
clear_and_set( compl_trn );
putrsUSART(" (FL: ");
putsUSART(itoa(clock_aa, time));
putrsUSART(")\n");
}
}
Timer value used in verification was a value
after guard evaluation followed by check synch
and before moving into next state
20
Multi-threaded C code Structure
 A thread per each transition
transV1
 Uses semaphores for each
location and each input
event
int main(…)
{
pthread_create(&threadV1,
NULL, transV1, NULL);
pthread_create(&threadV2,
NULL, transV2, NULL);
pthread_create(&threadV3,
NULL, transV3, NULL);
…
pthread_join ();
}
void *transV1(void *ptr)
{
while(1) {
Evaluate
sem_wait(&WaitRI);
guard
t=wait2(&v_x,&ri);
clearTimer(&v_x);
Update
current=ST_W_VRP;
sem_post(&WaitVRP);
sem_post(&Pace);
}
}
21
Multi-threaded Code Structure
transV1
task Template
while true
WaitEvent(CURR_LOC_EVENT);
ClearEvent(CURR_LOC_EVENT);
thread specific calculation
sleep when necessary
if ((sleeping is used) and
void *transV1(void *ptr)
(cur_loc is changed when waking up))
{
cancel transition
else
while(1) {
update variables
Evaluate
sem_wait(&WaitRI);
clear timer when necessary
guard
t=wait2(&v_x,&ri);
change to destination location
clearTimer(&v_x);
SetEvent(DEST_task_ID, EVENT_ID);
Update
current=ST_W_VRP;
perform verification
sem_post(&WaitVRP);
end if
sem_post(&Pace);
end while
}
}
22
Check Using Assertion
void *trans2 (void *ptr)
{
while(1)
{
sem_wait(&WaitRI);
t=wait2(&v_x,&ri,..)
if(t==-1) continue;
assert(&v_x,0);
// printf
clearTimer(&v_x);
sem_post(&WaitVRP
sem_post(&Pace)
}
}
void assert(struct timeval *tv,int id)
{
int t=getTimer(tv);
saved[saved_int]=t;
saved_id[saved_int]=id;
saved_int++;
}
23
Issues
 (1) Change the code minimally
 Which point of timer should be used for checking?
 Which delta value should we use?
 All tested scenarios  All possible scenarios
 Testing vs. verification
 (2) Change the model
 Can we assure that we made correct changes on model according to the
changes on code?
 Is it enough to change only corresponding guards in model?
 Do we also need to modify invariants in model?
24
Issues (cont.)
 (3) Check properties again
 We still feel less confident on that these changes to the code and model
really have no effects on property preservation
 Even huge delta value (e.g. 500ms) does not make properties violated
 Is our set of properties reasonably enough to catch all the important
properties of VVI mode?
 Do we need to improve our model and properties?
25
Implementation Goal
Goal
Generate C code guaranteeing properties transferred from the verified
model within specific bounds
Obstacles
 Instantaneous responses in the model are not implementable
 Models use continuous clocks and implementations use digital clocks with
finite precision
26
Code Synthesis & Timing Analysis
(1)
Timed
automata
model
Produce C code from the timed
automata model systematically
(3)
C code
synthesis
Check whether the timing properties are
satisfied in the code (by testing)
(4)
(2)
Measurement
based
timing analysis
Model checking
(with UPPAAL)
(5)
For each of violating properties,
measure how much deviations occur
 Find a timing tolerance ∆
Modify the code and the model with ∆
Re-checking
with ∆
Check again that the model and the
code satisfy all the properties within ∆
27
Code Synthesis
 Generated two flavors of implementation code
 Single-threaded
Thread support
 Multi-threaded
Single threaded C code
Timed
automata
model of a
pacemaker
Timing analysis
No thread support
Multiple threaded C code
Timing analysis
28
Single-threaded Code Structure
 One big loop
 Inspired by TIMES tool’s code generation
…
for each trn do
if (trn is active) and (eval_guard(trn))
if (there is synchronization)
if (compl_trn exists) and (eval_guard(compl_trn))
update variables of both trn and compl_trn;
take both trn and comp_trn to new states;
set trn to -1; /* check all outgoing transitions again */
end if
else
/* no synchronization */
update variables of trn;
take the transition trn to new state;
set trn to -1;
end if
end if
end for
…
29
Property Checking in Code
 Inserted “if-then-else” checking statement inside the loop for
the properties which should be satisfied all the times
 PropLRI: A[] (!Ventricle.hpenable imply Ventricle.x <=
Ventricle.LRI)
if(Ventricle_hpenable == false){
if(Ventricle_clock <= Ventricle_LRI){
print “T” and clock value;
}
else{
print “F” and clock value;
}
}
30
Property Checking by Testing in Code
 Performed simulation-based black box testing
CPU: Microchip PIC18F4520 (40 MHz)
 Compiler: MPLAB® C Compiler for PIC18 MCUs
 Triggered a pin interrupt manually to represent a heart sense

 Tested with sequences of test cases covering the following
scenarios
1.
2.
3.
4.
5.
Pacing–Pacing: >= LRI
Pacing–Sensing (during VRP): < VRP & < LRI
Pacing–Sensing (after VRP): >= VRP & < LRI
Sensing–Pacing: >= HRI
Sensing–Sensing: < HRI
0
320
(VRP)
31
1000
(LRI)
1200
(HRI)
Time (ms)
Result of Property Checking in Code
 Findings
 Code execution time harms property preservation
 Characteristics of timing properties matters
 clock_var  limit (e.g. PropVRP) are guaranteed
 clock_var  limit (e.g. PropLRI, PropHRI) are not guaranteed
 Time deviations were bounded in the tested scenarios (E.g.,  1ms)
32
Timing Tolerance ∆
 Modify the code and the model referring to the violated
properties to keep the properties transferred from the model in
the code satisfied
 Strategy for converting the violated properties to the satisfied
ones
Find a timing tolerance ∆ by measuring deviations from
the desired time
Make the desired events happen no later than the
predetermined time T by evaluating guard at ∆ time units
earlier than T, while not violating all other properties
33
Modify the Code with ∆
 To make guard evaluated ∆ time units earlier
#define DELTA
(some value)
…
bool eval_guard(int trn) {
switch(trn) {
case 0: return (Heart_flag>0);
case 2: return (rdClock(Ventricle_x)>=Ventricle_RI - DELTA;
case 4: return (rdClock(Ventricle_x)>=Ventricle_VRP);
… }
}
 Experimented using several values of ∆
 Three properties are satisfied in the code with ∆ greater than
or equal to 2ms for all tested scenarios
34
Modify the Model with ∆
 Make the corresponding changes in the model
x >= RI – DELTA
 Verify the modified model again w.r.t. all the properties
 Confirm that the modified model satisfies all the properties
with the timing tolerance
35
Result of Property Checking in Code
 Simulation-based black box testing on Linux
 Test inputs: Randomly generated heart sensing signals
 Execution delay was shown to be bounded by 2ms
: 2ms
First checking result
Re-checking result
36
Related Work: Code Gen. from TA
 TIMES tool [AFP+03]
 Generate code from TA extended with tasks for BrickOS platform
 Under synchrony hypothesis (SH), the code synthesis is guaranteed to preserve
safety properties transferred from models
  Supports enriched TA, provides many types of automatic analysis
  Preservation of properties is not guaranteed without SH
 ELASTIC2BRICK tool [DDR04]
 Generate code from a simplified TA for BrickOS platform
 Safety properties proven correct with Δ in the model are preserved
  Formalized treatment of the synchrony hypothesis and correctness proofs
  Limited and difficult applicability (e.g. no shared variables, no broadcasting,
etc.)
 Our approach
 Applicable without much restrictions while guaranteeing timing properties to
some extents without SH
37