Runtime verification: From theory to practice and back

Gordon Pace, Department of Computer Science, Faculty of ICT,  University of Malta

Course objectives

Runtime verification has proved to be one of the foremost formal methods to be palatable by industry. The increase in size and complexity of systems, while expecting more dependability, has been putting pressure on stronger verification and validation frameworks to ensure soundness. By verifying only the current execution path, and using specification logics for which single path verification is relatively cheap, runtime verification induces a relatively low cost to add runtime monitors to systems from an overheads perspective. Also, techniques used in quality control for testing lend themselves almost directly to runtime verification, resulting that the cost of retraining so as to have in-house expertise is also low.

In this course, we propose to present the ideas behind runtime verification from both a theoretical and practical perspective. The course starts by building a formal framework to characterise the technique used in runtime verification, but also adopts, in parallel, a hands-on approach with the students progressively constructing a runtime verification tool and applying it to a mock transaction
system.

The objectives of the course are threefold:

• Understand the concepts and theoretical underpinnings behind runtime verification.
• Understand the practical issues arising in implementing a runtime verification framework.
• Become aware of the current open questions and challenges in the field.

Course outline

1. What is verification?

This part of the course aims at presenting the students with the problem of verification — of how a system can be given formal semantics so as to enable analysis of its state space against given properties. Different verification techniques are presented within this formal framework, including (i) model checking; (ii) testing; (iii) (possibly) symbolic execution; and (iv) runtime verification. Furthermore, from a pragmatic viewpoint, these techniques are seen in the context of the development lifecycle, to analyse how these verification techniques feedback into the development process. In this manner, students will appreciate better what runtime verification is, especially within the context of verification and validation in general.

2. Choices for Features of Runtime Verification

The aim of this part of this course is to focus on runtime verification —looking at the choices and options in the design and setup of a monitoring framework. The choices which will be discussed will be split into three parts, each of which will be expanded on separately later:

• Monitoring architecture: Look into different options of how runtime verification interacts with the system: (i) synchronous vs. asynchronous monitoring; (ii) online vs. offline monitoring; (iii) pure monitoring vs. feedback to the system.
• Instrumentation: Unless explicitely inlined in the code, the instrumentation of monitors leads to changes in the system. The different approaches of (i) inlined assertions; and (ii) aspect-oriented programming, are discussed and compared.
• Logics for monitoring: Until this point in the course, only informal specifications will have been shown. The students are made aware of how different logics can be used to specify the monitor, and how properties written in such logics can be automatically compiled  into code implementing the monitor.

3. Instrumenting Monitors

The instrumentation phase is expanded upon, going into more concrete detail. This will be accompanied with a hands-on session getting the students to start implementing a small runtime verification tool which will be applied to a small case study.

• Assertion-based: A series of examples will be used to show students how assertion-based runtime verification can be used to verify properties with different complexity. Starting from a point property (e.g. the withdrawCash method is never called with a negative-valued parameter ) to an interval-based real-time property (e.g. in any half hour period, the user may not make more than 50 transactions). The loss of modularity and comprehensibility over these examples will motivate more sophisticated instrumenting techniques.
• Aspect-oriented programming: The killer application of aspect-oriented programming is almost certainly that of modularly instrumenting monitors in a system. An introduction to aspect-oriented programming will be given, including hands-on sessions using AspectJ to write Java aspects. The examples given in the assertion-based part will be reconstructed using AspectJ, showing greater modularity and abstraction.

4. Architecture of a Runtime Verification System

The architectural issues raised in the overview part of the course will be revisited, but implementing them for a deeper understanding of how it impacts the design. 

5. Logics for Runtime Verification

The advantage of runtime verification emerges when it enables the writing of complex properties using a high-level logic, and which can be automatically translated into a monitor. We will look at different logics and how they can be automatically compiled into monitors. The logics and specification languages covered are planned to be: (i) a point logic (pre/post-conditions); (ii) automata; (iii) past time logic (to study a finite trace logic); (iv) regular expressions; (v) linear time logic. If time permits, we will also look at timed properties using automata, and quantified (replicated) properties.

6. Other Issues in Runtime Verification

At this point of the course, through the lectures and the hands-on sessions, the students will have a good understanding of the underlying issues arising when using runtime verification. To close the course, we will be presenting short snapshots of a number of other non-core but interesting research directions in runtime verification. Areas proposed to be covered may include: (i) monitoring distributed systems; (ii) monitor-oriented programming; (iii) sampling and overhead reduction; (iv) testing and runtime verification; and (v) the problem of monitoring correctness (correct logic compilation, the observer effect and overheads due to logic complexity).

Course structure and assessment approach

The course has both a theoretical and a practical part. While parts 1, 2 and 6 of the course are almost exclusively lecture-based, parts 3–5 will be presented as a combined lecture and hands-on session, thus helping the students understand the hidden practical issues and aspects inherent in runtime verification.

The hands-on sessions will also serve to bootstrap the students’ assignment which will consist of building a runtime verification framework in Java and for Java programs, testing it on a given transaction-handling system. Students will be provided with the code which is peripheral to the monitoring aspect of the course (such as code to parse specifications) and will be asked to build upon it to develop the runtime verification tool.

A mock case-study will be used throughout the course to (i) illustrate concepts covered; and (ii) to test the students’ system over. The case-study consists of a transaction system mimicking multiple usersperforming financial transactions over various accounts. The case study will be used since it amply illustrates many interesting issues rising in runtime verification such as concurrent processes, replicated properties and stateful monitors.

Prerequisites

Students taking the course are expected to be (i) familiar with basic propositional and first-order logic; and (ii) competent Java programmers, ideally familiar with the Eclipse IDE.

El curso será dictado en inglés, pero el Prof. Pace puede responder consultas en castellano. La evaluación del curso consiste en un examen con modalidad "take-home", y puede incluir también ejercicios dados durante las clases prácticas del curso.

Dado que este curso se dictará en un laboratorio, la vacante no está confirmada si no se realiza el pago de la inscripción.

Acerca del profesor

Gordon J. Pace is an associate professor, heading the Department of Computer Science of the University of Malta. He previously also worked at Chalmers University, Laboratoire Verimag and INRIA. His research interests include formal methods for software and hardware, runtime verification and the formal analysis of contracts. Apart from an interest in the theoretical underpinnings of runtime verification, he has been involved in the development of a number of runtime verification tools and their application to industrial case studies - upon which the course which will be delivered is based.