A Survey ofRuntime Verification.ppt

A Survey of Runtime Verification Jonathan Amir 2004 2 Background ? Model checking: ? Formal, sound, provides guarantees. ? Doesn ’ t scale well - state explosion problem. ? Checks a model, not an implementation. ? Some people fear it – too much formalism. ? Software testing (ad-hoc checking): ? Most widely used technique in the industry. ? Scales well, usually inexpensive. ? Test an implementation directly. ? Informal, doesn ’ t provide guarantees. 3 Runtime Verification ? Attempt to bridge the gap between formal methods and software testing. ? A program is monitored while it is running and checked against properties of interest. ? Properties are specified in a formal notation. ? Dealing only with finite traces. ? Considered as a light-weight formal method technique. ? Testing with formal “ flavour ”. ? Still doesn ’ t provide full guarantees. 4 Runtime Verification, cont ’d ? How to monitor a program? ? Need to extract events from the program while it is running. ? code instrumentation. Static phase Dynamic phase Program Specifications Code Instrumentation Instrumented Program Runtime Checker Stream of events 5 ? Property of interest is [](x>0) . ? Search code for assignments to x. ? Insert code stubs municate with the monitor. ? Three means munication: ? Networking. ? Shared memory. ? File system. An (informal) example x = 5 // code stub here // reports to monitor …… x = -1 // code stub here // reports to monitor. // monitor detects // violation 6 Finite traces ? Trace semantics are different for finite traces. ? Can fake infinite trace by stuttering. ? Stutter the last state, or ? stutter a “ dummy ” state that doesn ’ t fulfill any proposition. ? Problem: meaning of [] operator changes. ? A more accepted alternative: define different acceptance condition. 7 Finite traces, Cont ’d ? Acceptance condition: A trace is acceptable if all its eventualities have been fulfilled. ? Example: [](x -> <>y) . ? What if every occurrence of x is followed by