Runtime Verification or Verification over Finite Paths
Description
The major goal of runtime verification is the application of verification
techniques to finite executions of a system.
Possible applications:
-
Temporal assertions:
Extending the language of assertions to a temporal logic. This provides
a superset over currently available language assertions (for example, assert
keyword
in Java), and watches in the debugger. Additional expressive power makes
it possible to express temporal dependencies between different states of
the program. For example, if at some point x and y are positive, then x
remains positive from this point on.
- Verification of a simulation run:
Simulation is the most widely used testing approach in hardware industry.
Combining simulation with runtime verification shortens the verify-check-fix
cycle. Using the same logic to specify runtime properties as static properties
decreases the cost of verification.
- Debugging Aid:
The technique can be applied to any trace produced by a debugger, potentially
helping to identify an interesting part.
- Runtime Program Monitoring:
A runtime verifier can be embedded with the actual program to aid in
future maintenance. This is similar to always keeping the assertions in
the program.
Related Work
-
three workshops on run-time verification (RV1-RV3). At least the
last one was associated with CAV'03.
-
finite trace semantics (one needs to provide finite trace semantics to
temporal logics in order to extend model-checking techniques to finite
paths). A few attempts have been reported in TACAS'03, CAV'03, RV'03,
CONCUR'03.
-
runtime program monitoring.
-
Our work on XChek: Marsha Chechik, Benet Devereux,
Arie Gurfinkel, Steve Easterbrook.
Multi-Valued Symbolic Model-Checking. To appear in
Transactions on Software Engineering and Methodology, 2003.
-
Arie Gurfinkel, Marsha Chechik. Proof-Like Counter-Examples, Proceedings of TACAS, April 2003.
Current Status of the Project:
A lot of our efforts over the next two years will be in this area. There are
several funded projects to apply these ideas, and we are actively looking
for students to carry this work out. See me for more details.
Last updated: Sept. 3, 2003