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.
Author(s): Cindy Eisner (auth.), Oleg Sokolsky, Serdar Taşıran (eds.)
Series: Lecture Notes in Computer Science 4839
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2007
Language: English
Pages: 218
Tags: Software Engineering; Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs; Management of Computing and Information Systems
Front Matter....Pages -
PSL for Runtime Verification: Theory and Practice....Pages 1-8
On the Semantics of Matching Trace Monitoring Patterns....Pages 9-21
Collaborative Runtime Verification with Tracematches....Pages 22-37
Static and Dynamic Detection of Behavioral Conflicts Between Aspects....Pages 38-50
Escaping with Future Variables in HALO....Pages 51-62
Runtime Verification of Interactions: From MSCs to Aspects....Pages 63-74
Towards a Tool for Generating Aspects from MEDL and PEDL Specifications for Runtime Verification....Pages 75-86
ARVE: Aspect-Oriented Runtime Verification Environment....Pages 87-96
From Runtime Verification to Evolvable Systems....Pages 97-110
Rule Systems for Run-Time Monitoring: From Eagle to RuleR ....Pages 111-125
The Good, the Bad, and the Ugly, But How Ugly Is Ugly?....Pages 126-138
Translation Validation of System Abstractions....Pages 139-150
Instrumentation of Open-Source Software for Intrusion Detection....Pages 151-163
Statistical Runtime Checking of Probabilistic Properties....Pages 164-175
Temporal Assertions with Parametrised Propositions....Pages 176-187
Rollback Atomicity....Pages 188-201
Runtime Checking for Program Verification....Pages 202-213
Back Matter....Pages -
