MaC Monitoring and Checking at Runtime (Continue)Recap: MaCMaC Verifier and LanguageEventsConditionsCurrent WorkRegular Expressions in MEDLChallengesIdentify which events are relevantExample: no sends after readMaC with Regular ExpressionsOverlapping RESimultaneous EventsProbabilistic PropertiesStatistical Technique1. Simulate and 2. Collect SampleMaC Probabilistic PropertiesExample3. Estimating ProbabilitySlide 20Statistical Hypothesis TestingProbability Estimation: Z-ScoreContinue…Dynamic MaCMaCMonitoring and Checking at Runtime(Continue)Presented ByUsa SammapunCIS 700 Oct 12, 2005Recap: MaC►Runtime verification technique–Ensures the current program execution follows its formal requirements at run-timeInstrumentedProgramEventRecognizerChecker InjectorMaC VerifierExecution info variable update method call/returnEventsConditionsViolationsFeedbackMaC Verifier and LanguageProgramMaC CompilerPEDL MEDLMaC SpecificationSADLWhere/when to steerSystem Properties using EVENTS and CONDITIONSMap variable update, method call/return to EVENTS and CONDITIONSEvents►e - variable update, start/end method►e1 || e2 - or►e1 && e2 - and►start(c) - instant when condition c becomes true►end(c) - instant when condition c becomes false►e when c - e occurs when condition c is true►Alarms: events that must never occurConditions►Conditions interpreted over 3 values: true, false and undefined.►c - boolean expression►!c - not c►c1 || c2 - or►c1 && c2 - and►c1 -> c2 - imply►defined(c) - true when c is defined►[e1, e2) - interval►Safety Properties: conditions that must always hold trueCurrent Work►Timing properties:►Regular expressions►Probabilistic properties►Dynamic MaCd}{21)e,[ed}{21 )e,[e d}{21)e,[eRegular Expressions in MEDL►MEDL is based on temporal logic►Regular expressions (RE) may be better –Engineers understand them–More concise than TL for temporal ordering►RE ranges over MaC events–event a,b,c–a.b*.cChallenges►When to accept several possible inputs (ab*c*)–Shortest input–Longest input–All input►Identify which events are relevant►Overlapping RE►Simultaneous eventsIdentify which events are relevant►An unexpected event fails the RE check►Trace may contain “irrelevant” events, which should not make RE failExample: no sends after readopen.send*.read*.close►Which traces should be accepted or rejected?–open.send.read.close accept–open.send.read.send.close reject–open.send.send.read continue–open.send.delete ?reject–open.send.chdir.close ?acceptRE fileaccess{open,send,close,delete} = open.send*.read*.closeMaC with Regular Expressions►Regular expression over events–Statement: RE R {Ē} = < R >, –Grammar of R: R ::= e | R.R | R+R | R*–Relevant set {Ē}: contribute to RE failure►RE are neither events nor conditions–Events associated with RE R:startR(R), success(R), fail(R) ►alarm badAccess = fail(fileaccess)Overlapping RE►Property: open.send*.read*.close►Trace: –Actual: open open send read send read –We see: open open send read send read ►Cannot distinguish between two overlapping instances; events miss attribution–What is the right way to index events?Simultaneous Events►Checker operates on a stream of observations–Observations are primitive events that reflect change of system state►One primitive event can trigger different other events►What if those events are in the the same RE–a . (a || b) . b–at state i, a occurs, then (a || b) also occurs–How do we order a and (a || b)Probabilistic Properties►Probability calculation–Numerical technique–Statistical technique1. Simulate2. Collect several samples3. Estimate probabilitiestask startfinish in 800.250.75finish in 100not finish in 100not finish in 800.20.8Statistical Technique►usually, we 1) execute for X times, 2) use them as samples, and 3) estimate probabilitiestask start finish in 100not finish in 100task starttask start finish in 100task start finish in 100task start finish in 100…1. Simulate and 2. Collect Sample►runtime verification – only one execution pathtask start finish in 100not finish in 100task starttask start finish in 100task start finish in 100task start finish in 100server start update vclient requestupdate v……task start finish in 100not finish in 100task starttask start finish in 100task start finish in 100 task start finish in 100MaC Probabilistic Properties►Experiment–An element that indicates a sub-path•eexp ( previous example: task start )•cexp►Probabilistic event ◉ = {<, >, ≤, ≥, =, ≠}–e prob( ◉p, eexp)►Probabilistic condition–c prob( ◉p, cexp)Example►A soft real-time task must not miss a deadline of 100 time units with probability ≥ 0.2event missDeadline = end([startT,endT){≤100}) alarm soft_rt_task = missDeadline prob(≥ 0.2, startT)►A car velocity must be < 50mph with prob ≥ 0.9 in work zonesproperty speed = (v < 50) prob(≥ 0.9, work_zone)3. Estimating Probability►Estimate probability from program execution –compute experimental probability p’condition and p’event –Condition: c prob( < p, cexp) Event: e prob( < p, eexp) ►A car velocity must be < 50mph with prob ≥ 0.9 in work zones  (v < 50) prob(≥ 0.9, work_zone)|e of soccurrence||e of soccurrence|p'expevent |truec s.t. S||truec s.t. S|p'expiiconditiontrue e work_zon:states#true 50) (v :states #p'conditionExampleevents start task #events deadline miss #p' event 0 1p=0.2 p’=0.267► task must not miss a deadline of 100 time units with probability ≥ 0.2  alarm soft_rt_task = missDeadline prob(≥ 0.2, startT)  # miss deadline events = 40 # startT (task start events) = 150 p’ = 40 / 150 = 0.267Statistical Hypothesis Testing►Given–Probability estimation–Confidence interval (CI) e.g. CI = 95%►Statistical Hypothesis Testing–Satisfied–Not satisfied–Need more sampleProbability Estimation: Z-Score►Use z-score to calculate how far apart p and p’ areFor event, n = |occurrences of eexp|For condition, n = |Si s.t. cexp = true|• Sign of z says which direction + z says p’ > p - z says p’ < p• Value of z says how far apart p’ and p ► task must not miss a deadline of 100 time units with probability ≥ 0.2  p =