Runtime Verification

1. Front Matter

   PDF

2. Invited Paper

   1. PSL for Runtime Verification: Theory and Practice

      • Cindy Eisner

      Pages 1-8

3. AOP-Related Papers

   1. On the Semantics of Matching Trace Monitoring Patterns

      • Pavel Avgustinov, Julian Tibble, Oege de Moor

      Pages 9-21

   2. Collaborative Runtime Verification with Tracematches

      • Eric Bodden, Laurie Hendren, Patrick Lam, Ondřej Lhoták, Nomair A. Naeem

      Pages 22-37

   3. Static and Dynamic Detection of Behavioral Conflicts Between Aspects

      • Pascal Durr, Lodewijk Bergmans, Mehmet Aksit

      Pages 38-50

   4. Escaping with Future Variables in HALO

      • Charlotte Herzeel, Kris Gybels, Pascal Costanza

      Pages 51-62

   5. Runtime Verification of Interactions: From MSCs to Aspects

      • Ingolf H. Krüger, Michael Meisinger, Massimiliano Menarini

      Pages 63-74

   6. Towards a Tool for Generating Aspects from MEDL and PEDL Specifications for Runtime Verification

      • Omar Ochoa, Irbis Gallegos, Steve Roach, Ann Gates

      Pages 75-86

   7. ARVE: Aspect-Oriented Runtime Verification Environment

      • Hiromasa Shin, Yusuke Endoh, Yoshio Kataoka

      Pages 87-96

4. Core Runtime Verification Papers

   1. From Runtime Verification to Evolvable Systems

      • Howard Barringer, Dov Gabbay, David Rydeheard

      Pages 97-110

   2. Rule Systems for Run-Time Monitoring: From Eagle to RuleR

      • Howard Barringer, David Rydeheard, Klaus Havelund

      Pages 111-125

   3. The Good, the Bad, and the Ugly, But How Ugly Is Ugly?

      • Andreas Bauer, Martin Leucker, Christian Schallhart

      Pages 126-138

   4. Translation Validation of System Abstractions

      • Jan Olaf Blech, Ina Schaefer, Arnd Poetzsch-Heffter

      Pages 139-150

   5. Instrumentation of Open-Source Software for Intrusion Detection

      • William Mahoney, William Sousan

      Pages 151-163

   6. Statistical Runtime Checking of Probabilistic Properties

      • Usa Sammapun, Insup Lee, Oleg Sokolsky, John Regehr

      Pages 164-175

   7. Temporal Assertions with Parametrised Propositions

      • Volker Stolz

      Pages 176-187

   8. Rollback Atomicity

      • Serdar Tasiran, Tayfun Elmas

      Pages 188-201

   9. Runtime Checking for Program Verification

      • Karen Zee, Viktor Kuncak, Michael Taylor, Martin Rinard

      Pages 202-213

5. Back Matter

   PDF

Runtime veri?cation is a recent direction in formal methods research, which is complementary to such well-established formal veri?cation methods as model checking. Research in runtime veri?cation deals with formal languages suitable for expressing system properties that are checkable at run time; algorithms for checking of formal properties over an execution trace; low-overhead means of extracting information from the running system that is su?cient for checking of the property. Applications of runtime veri?cation technology include po- deployment monitoring of system correctness and performance; construction of formally speci?ed test oracles; collection of statistics about system behavior, among others. The Workshop on Runtime Veri?cation was started in 2001 and has been held annually since then. The workshop was co-located with the Conference on Computer-Aided Veri?cation (CAV) in 2001–2003 and 2005–2006;and with the European Joint Conferences on Theory and Practice of Software (ETAPS) in 2004. In 2007, the workshop was held on March 13, 2007 in Vancouver, British Columbia, Canada, co-located to the Conference on Aspect-Oriented Software Development (AOSD) in order to explore the emerging connections between the two communities.

• Aspect-oriented programming
• Open-Source
• Variable
• abstract state machines
• aspect oriented programming
• automated testing
• correct systems design
• domain specific language
• fault diagnosis
• finite state machines
• interactive testing
• object oriented design
• programming
• semantics
• verification

Policies and ethics