RV'07 - Seventh Workshop on
Satellite workshop of AoSD'07.
Runtime Verification
March 13, 2007
Vancouver, British Columbia, Canada
*** Instructions for submitting full papers for the post-proceedings ***
The objective of RV'07 is to bring scientists from both academia and industry together to debate on how to monitor and analyze the execution of programs, for example by checking conformance with a formal specification written in temporal logic or some other form of history tracking logic. The purpose might be testing a piece of software before deployment, detecting errors after deployment in the field and potentially triggering subsequent fault protection actions, or the purpose can be to augment the software with new capabilities in an aspect oriented style. The longer term goal is to investigate whether the use of lightweight formal methods applied during the execution of programs is a viable complement to the current heavyweight methods proving programs correct always before their execution, such as model checking and theorem proving. This year's workshop is organized as a satellite event of AOSD to specifically create a synergy between the fields of runtime verification and aspect oriented programming. Within the recent few years a trend has emerged in the aspect oriented community to extend pointcut languages to richer trace predicate languages, including regular expressions, state machines, temporal logic and grammars. This trend obviously invites to a future synergy between the two fields since runtime verification studies exactly these kinds of problems.
The subject covers several technical fields as outlined below.
Specification Languages and Logics. Formal methods scientists have investigated logics and developed technologies that are suitable for model checking and theorem proving, but monitoring can reveal new observation-based foundational logics.
Aspect-oriented Languages with Trace Predicates. New results in extending aspect languages, such as for example AspectJ, with trace predicates replacing the standard pointcuts. Aspect oriented programming provides specific solutions to program instrumentation and program guidance.
Program Instrumentation in General. Any techniques for instrumenting programs, at the source code or object code/byte code level, to emit relevant events to an observer.
Program Guidance in General. Techniques for guiding the behavior of a program once its specification is violated. This ranges from standard exceptions to advanced planning.
Combining Static and Dynamic Analysis. Monitoring a program with respect to a temporal formula can have an impact on the monitored program, with respect to execution time as well as memory consumption. Static analysis can be used to minimize the impact by optimizing the program instrumentation. Runtime monitors can be seen as proof obligations left over from proofs - what is left that could not be proved.
Dynamic Program Analysis. Techniques that gather information during program execution and use it to conclude properties about the program, either during test or in operation. Algorithms for detecting multi-threading errors in execution traces, such as deadlocks and data races. Algorithms for generating specifications from runs -- dynamic reverse engineering, can include program visualization.
Both foundational and practical aspects of monitoring were encouraged.
Previous workshops:
RV'01 First Workshop on Runtime Verification, Paris, France, July 2001 RV'02 Second Workshop on Runtime Verification, Copenhagen, Denmark, July 2002 RV'03 Third Workshop on Runtime Verification, Boulder, USA, July 2003 RV'04 Fourth Workshop on Runtime Verification, Barcelona, Spain, April 2004 RV'05 Fifth Workshop on Runtime Verification, Edinburgh, Scotland, July 2005 FATES/RV'06 First Joint Workshop on Formal Aspects of Testing and Runtime Verification, Seattle, USA, August 2006