RV 2010

Cyrille Valentin Artho. Run-time Verification of Networked Software Abstract: Most applications that are in use today inter-operate with other applications, so-called peers, over a network. The analysis of such a distributed application requires that the effect of the communication with peers is included. This can be achieved by writing or generating stubs of peers, or by including all processes in the execution environment. We also present an alternative approach, which analyzes a networked application by recording and caching its communication with peers. Caching becomes useful when several traces of the application are analyzed. It dispenses with the need of generating a new peer application execution for each different execution of the main application. Such a caching framework for input/output has been implemented on the Java PathFinder platform, which can be used to verify executions of non-deterministic applications at run-time.
Eric Bodden and Patrick Lam. Clara: Partially Evaluating Runtime Monitors at Compile Time Abstract: Researchers have developed a number of runtime-verification tools that generate runtime monitors in the form of AspectJ aspects. In this tutorial, we present Clara, a novel framework to statically optimize such monitoring aspects with respect to a given program under test. Clara uses a sequence of increasingly accurate static analyses to automatically convert a monitoring aspect into a residual runtime monitor that only monitors events triggered by program locations that the analyses failed to prove safe at compile time. If the static analysis succeeds on all locations, this proves that the program fulfills the stated properties, which completely obviates the need for runtime monitoring. Otherwise, the residual runtime monitor is usually much more efficient than a full monitor, but nevertheless guaranteed to capture all property violations at runtime. In this tutorial, attendees will learn about all important concepts and design decisions of the Clara framework. We will explain the internal workings of Clara’s different static analyses, and how researchers can integrate Clara’s static analyses with their own runtime-monitoring tools. Also, we will explain how to extend Clara with custom static analyses. More information at: http://www.bodden.de/2010/05/18/clara-tutorial/
Ylies Falcone. You should Better Enforce than Verify Abstract: This tutorial deals with runtime enforcement which is an extension of runtime verification aiming to circumvent misbehaviors of programs. Within this technique the monitor not only observes the current program execution, but it also modifies it. It uses an internal memory, in order to ensure that the expected property is fulfilled: it still reads an input sequence but now produces a new sequence of events in such a way that the property is enforced. The precise and formal relation between input and output sequences is usually ruled by two constraints: soundness and transparency. From an abstract point of view those constraints entail the monitor to minimally modify the input sequence in order to ensure the desired property. This tutorial focuses on runtime enforcement and advocates its use as an extension to runtime verification. More specifically the tutorial steps are the following: 1) we overview previous approaches to runtime enforcement; 2) we thoroughly present our latest advances in runtime enforcement that generalizes and extends previous approaches; 3) we discuss practical limitations and future challenges.
Sylvain Hallé and Roger Villemaire. Runtime Verification for the Web Abstract: Web service message contracts are constraints on the values and sequences of XML messages that can be exchanged between a client’s web browser and an application server. This tutorial presents BeepBeep, a lightweight Java monitor that can check and enforce message contracts expressed as LTL formulae with first-order quantification over data fields. Its use is illustrated on real world web applications submitted to these kinds of contracts.
Axel Legay. Statistical Model Checking: Present and Future Abstract: Quantitative properties of systems are usually specified in logics that allow one to compare the measure of executions satisfying certain temporal properties with thresholds. The model checking problem for systems with respect to such logics is typically solved by a numerical approach that iteratively computes the exact measure of paths satisfying relevant subformulas; the algorithms themselves depend on the class of systems being analyzed as well as the logic used for specifying the properties. Another approach to solve the above problem is to simulate the system for finitely many runs, and use hypothesis testing to infer whether the samples provide a statistical evidence for the satisfaction or violation of the specification. In this tutorial, we will survey this "Statistical Model Checking" (SMC) approach and we will present real-world applications for which it is the only viable solutions: Systems Biology (size), Signal convertors (properties that cannot be expressed in temporal logic but that can be checked on an execution), Heterogenous Systems (new classes of monitors). We will also put SMC in perspective with Runtime Verification (RV). The common concept between RV and SMC is that of monitoring an execution with respect to some given property. Like RV, SMC does not assume the existence of a mathematical model for the system to be verified, but rather view it as a box that produces outputs. So far, SMC has mostly been used to verify reachability properties and solutions for liveness properties are missing. We hope that solutions developed in the RV area could be used in the SMC area. This tutorial may be a chance to create interactions between these two worlds.
Patrick Meredith and Grigore Rosu. Runtime Verification with the RV System Abstract: The RV system is the first system to merge the benefits of Runtime Monitoring with Predictive Analysis. The Runtime Monitoring portion of RV is based on the successful Monitoring Oriented Programming system developed at the University of Illinois, while the Predictive Analysis capability is a vastly expanded version of the jPredictor System also developed at the University of Illinois. With the RV system, runtime monitoring is supported and encouraged as a fundamental principle for building reliable software: monitors are automatically synthesized from specified properties and integrated into the original system to check its dynamic behaviors. When certain conditions of interest occur, such as a violation of a specification, user-defined actions will be triggered, which can be any code from information logging to runtime recovery. The RV system supports the monitoring of parametric properties that may specify a relationship between objects. Properties may be defined using one of several logical formalisms, such as: extended regular languages, context-free patterns, deterministic finite state machines, linear temporal logic, and past time linear temporal logic. The system is designed in such a way that adding new logical formalisms is a relatively simple task The predictive capabilities allow any of these monitoring specifications to be extended to checking not just the actual runtime traces of program execution, but any trace that may be inferred from a constructed casual model. The Predictive Analysis also features built in algorithms for race detection, atomicity violations, and deadlocks that are both highly useful in concurrent system design and difficult to specify in terms of formal specification languages. This tutorial will cover both the underlying concepts and the use of the RV system.