PACEMAKER Project Overall Plan (v0.5)

PACEMAKER Project Overall Plan (v0.5)

The 11th KOCSE Technical Symposium 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 timeguaranteed real-time software from a verified model? Present a safety-assured development approach for real3 time software 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 VR P

LRI VR P VR P HRI (> LRI) VR P LRI: Lower Rate Interval (e.g., 1000ms) HRI: Hysteresis Rate Interval (e.g., 1200ms) VRP: Ventricular Refractory Period (e.g., 320m 5 A Safety-Assured Development Software life cycle Development process

Requirement analysis Design (1) Timed automata model System spec. 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 Ventricul ar 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)

All these properties were satisfied Deadlock freeness A[] (not deadlock) on the model We assume that users capture all the important properties correctly. 8 Code Synthesis & Timing Analysis (1) Timed automata model (3) synthesis C code Check whether the timing properties are satisfied in the code (by testing)

(4) Measurement (2) Model checking (with UPPAAL) Produce C code from the timed automata model systematically (5) based timing analysis Re-checking with For each of violating properties, measure how much deviations occur

Find a timing tolerance Modify the code and the model 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 #define DELTA (some value) was set as 2ms in our case bool eval_guard(int trn) { Relax guard in the code switch(trn) { with case 0: return (Heart_flag>0); case 2: return (rdClock(Ventricle_x)>=Ventricle_RI - DELTA; case 4: return (rdClock(Ventricle_x)>=Ventricle_VRP); ... 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. 269300, 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. 139156.

[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. 273288. 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 for each trn if (trn if do is active) and (eval_guard(trn)) (there is synchronization) exists) and (eval_guard(compl_trn))

Timer value used in if (compl_trn read test_clock; checking is a value /* for property checking */ update variables of both trn and compl_trn; after guard take both trn and comp_trn to new states; evaluation followed check properties and print results; /* for property checking */ by check_synch and set trn to -1; /* check all outgoing transitions again */ before taking to end if else /* no synchronization */ next state 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 /********** verification *****************/ void check_trans() { for(trn=0; trn -1 ) { if( (compl_trn = check_synch( trans[trn].sync )) ) { 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); putrsUSART(" (FL: ");

putsUSART(itoa(clock_aa, time)); 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(")\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 transV1 transition 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 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); } } task Template while true WaitEvent(CURR_LOC_EVENT); ClearEvent(CURR_LOC_EVENT); thread specific calculation sleep when necessary if ((sleeping is used) and (cur_loc is changed when waking up)) cancel transition else update variables clear timer when necessary change to destination location SetEvent(DEST_task_ID, EVENT_ID); perform verification end if 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 within verified model bounds specific 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 (3) synthesis C code Check whether the timing properties are satisfied in the code (by testing) (4) Measurement (2) Model checking (with UPPAAL)

Produce C code from the timed automata model systematically (5) based timing analysis Re-checking with For each of violating properties, measure how much deviations occur Find a timing tolerance Modify the code and the model 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 Multi-threaded Timed automata model of a pacemaker Thread support Single threaded C code Timing analysis No thread support Multiple threaded C code Timing analysis 28 Single-threaded Code Structure One big loop Inspired by TIMES tools code generation

for each trn if (trn if do is active) and (eval_guard(trn)) (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. PacingPacing: >= LRI PacingSensing (during VRP): < VRP & < LRI PacingSensing (after VRP): >= VRP & < LRI SensingPacing: >= HRI SensingSensing: < HRI 0

320 (VR 31 100 0 120 0 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 37 broadcasting, etc.)

Recently Viewed Presentations

  • Statistics 202: Statistical Aspects of Data Mining Professor

    Statistics 202: Statistical Aspects of Data Mining Professor

    Definitions: Itemset A collection of one or more items Example: {Milk, Bread, Diaper} k-itemset = An itemset that contains k items Support count ( ) Frequency of occurrence of an itemset E.g. ({Milk, Bread,Diaper}) = 2 Support Fraction of transactions...
  • School of ITEE 4th year thesis/project Library research

    School of ITEE 4th year thesis/project Library research

    PowerPoint Presentation Start with a research plan Subject guides Information sources and search tools Some relevant databases Search strategies - using and linking keywords Example searches Refine search results by: Scopus PowerPoint Presentation PowerPoint Presentation PowerPoint Presentation Referencing software- EndNote...
  • Breaking Down the Prompt - HCPS Blogs

    Breaking Down the Prompt - HCPS Blogs

    These are two very important key words. A common mistake would be to write about many goals, even though the prompt tells you to focus on only one goal. Another common mistake would be to discuss goals that you want...
  • New York State Department of Transportation

    New York State Department of Transportation

    New York State Department of Transportation Kendrick Road Bridge Over I-390 Design-Build Project Request for Qualifications Informational Meeting June 27, 2012 Kendrick Road Bridge Agenda Introductions and Opening Remarks Project Overview Questions and Answers Peter Russell Att: Kendrick Road ...
  • The Hearts of the Homeless - Maryland

    The Hearts of the Homeless - Maryland

    PATH. Created under the McKinney-Vento Act, The PATH (Projects for Assistance in Transition from Homelessness) Program, is a formula grant program that funds the 50 States, District of Columbia, Puerto Rico, and four U.S. Territories to support service delivery to...
  • Poster Title Goes Here author&#x27;s name Seton Hall University ...

    Poster Title Goes Here author's name Seton Hall University ...

    Bruce Macfarlane, Ourania Filippakou, Liz Halford, Arti Saraswat Thames Valley University Attitudes to duality Traditionalists See further and higher education as representing distinct entities with different educational values, purposes and cultures Protectionists
  • PowerPoint-Präsentation

    PowerPoint-Präsentation

    By Stefan Rummel 05/05/2008 Prof. Rudowsky CIS 9.5 Brooklyn College Observing nature to find new solutions Observing behaviour of social insects Living in swarms Transfer behaviour to artificial models Explaining swarm intelligence using ants as an example Explaining swarm intelligence...
  • Grid, Globus Toolkit, and OGSA

    Grid, Globus Toolkit, and OGSA

    Open Grid Services as an Enabler of Future Networked Applications Ian Foster Argonne National Laboratory University of Chicago http://www.mcs.anl.gov/~foster