Titles and Abstract – 2nd school on Runtime Verification

Wolfgang Ahrendt (Chalmers University of Technology, Sweden) – slides

The Java Modeling Language – a Basis for Static and Dynamic Verification

The Java Modelling Language (JML) is specification language tailored for Java, using concepts from first-order logic to describe data invariants and pre-post conditions. It is used for both static and dynamic verification. The lecture will introduce JML as a language, JML based static verification using the KeY system, and JML based runtime assertion checking using openJML. Finally, I briefly mention the integration of JML concepts into an automata based paradigm, used for combined static and runtime verification.

Christian Colombo (University of Malta, Malta) – slides

Industrial Experiences with Runtime Verification of Financial Transaction Systems: Lessons Learnt and Standing Challenges

Applying runtime verification in industry has its particular challenges. This session aims to draw upon our ten years’ experience of applying runtime verification in industrial settings, in particular on financial transaction systems, to provide insights into questions such as: how runtime verification can be introduced in the software development lifecycle, who are the people to be involved and when, what kind of properties have been found useful in practise, and how these were monitored to keep intrusion to a minimum. The lecture ends by outlining a number of challenges which still need to be addressed for runtime verification to become more mainstream in industrial settings.

Alexandre Donze (DECYPHIR Inc., France) – slides

Monitoring Cyber-Physical Systems

Cyber-Physical Systems (CPS) are computerized systems interacting with their physical environments. They are prominent in transportation (car, plane, rockets), robotics, internet of things, etc. Real time and physical characteristics (such as velocities, temperatures, etc)  are an integral part of their functioning and their design, and as such, being able to measure and monitor these quantities in conjunction with the digital states of their embedded processing units is an important problem. In this talk, I will present some challenges and techniques based on extensions of formal methods adapted to the monitoring of CPS behaviors along with applications to their design and verification.

Adrian Francalenza (University of Malta, Malta) – slides

An Introduction to Runtime Verification and Monitorability

Runtime Verification is a lightweight technique that complements other verification methods in a multi-pronged approach towards ensuring software correctness. The technique poses novel questions to software engineers such as how to adequately check for a specified property at runtime and whether there are properties that cannot be runtime verified. In this tutorial, we strive towards a foundational understanding of these questions. This enables us to distill core concepts that can be extrapolated to various runtime verification settings. Particularly, we consider a specification logic that is agnostic of the verification method used but, at the same time, is general enough to embed commonly used specification logics. We also present an operational view of the main elements making up a typical monitoring framework. This allows us to establish a correspondence between the property satisfactions in the logic and the verdicts reached by the monitors carrying out the analysis. We also show how this correspondence is used to identify which subsets of the logic can be adequately monitored for. In this exposition we shall assume no prior knowledge of the specification logic or the monitoring framework considered.

Nikolai Kosmatov (CEA, France) – slides

Combined static and dynamic analyses in Frama-C: An Overview

Initially considered as orthogonal research fields, static and dynamic analysis techniques have been for a long time used separately to improve the quality of software. However, the development of both approaches has lead to the discovery of common issues and to the realization of potential synergies. The present talk gives an overview of some of the combinations between static and dynamic verification approaches that were realized in the context of Frama-C, a framework for static and dynamic analysis of C programs developed at CEA LIST.

First, we illustrate how static analysis can be used to help test generation.  The SANTE tool takes advantage of abstract interpretation and  program slicing in order to achieve more precise detection of runtime errors. These ideas have been pushed further in the LTest tool
in order to optimize automatic test generation for a large class of coverage criteria, through the detection of  infeasible test objectives.

Second, we illustrate how test generation can in turn help static analysis. We explore in the StaDy tool how program proof and test generation can be combined in order to help the validation engineer to understand and to fix proof failures during deductive verification of

Finally, we show how runtime verification can take benefit of static analysis in order to avoid the monitoring of irrelevant variables and statements (E-ACSL tool).

Martin Leucker (University of Lubeck, Germany)

In this tutorial we give an introduction to the field of Runtime Verification. More specifically, we give a comprehensive and coherent assessment of Linear Temporal Logic-based monitor synthesis approaches. We cover both rewriting and automata-based techniques from a propositional perspective and give a brief outlook to further topics related to runtime verification.

Joao Lourenco (University of Lisbon, Portugal) – slides

Discovering Concurrency Errors

Lots of concurrent software is being developed for the now ubiquitous multicore processors. And concurrent programming is difficult because it is quite easy to introduce errors that are really hard to diagnose and fix. One of the main obstacles to concurrent programming is that threads are scheduled nondeterministically and their interactions may become hard to predict and to devise. In this lecture we will address the nature of concurrent programming and some classes of concurrency errors. It discusses the application of dynamic program analysis techniques to detect, locate and diagnose some common concurrency errors like data races, atomicity violation and deadlocks. We will also discuss some techniques that can help with quality assurance of concurrent programs, regardless of any particular class of concurrency errors, like noise injection and systematic testing.

Gordon J. Pace (University of Malta, Malta) – slides

A Hands-On Introduction to Building a Runtime Verification Tool

This talk will take a hands-on approach to show how a runtime verification tool can be built from scratch, looking both at how the monitoring code can be automatically instrumented into a system, and how the monitoring logic can be extracted from a specification. For the former we will look at manual instrumentation and using aspect-oriented programming techniques, while for the latter we will look at how monitoring code can be synthesised from automata and regular expressions. The lecture will provide a grounding to the students in order to be able to follow how the techniques and results in other sessions can be integrated with real-world systems.

Laurence Pierre (Univ. Grenoble Alpes, France) – slides

Runtime Assertion-Based Verification for Hardware and Embedded Systems

With the increasing complexity of embedded systems, design verification can take up to 70% of the overall design time. Reducing time needed for verification is necessary due to time-to-market pressure. Runtime Assertion-Based Verification (ABV) is a methodology that enables ensuring that the behavior of a design meets its specification, from its earliest design stages. In that context the intended behaviour is formalized as logic and temporal assertions, expressed using IEEE standard languages such as PSL (IEEE std 1850), and automatically verified during simulation.
ABV for synchronous hardware IP blocks given as RTL (Register Transfer Level) descriptions has now widely gained acceptance. Various solutions have been developed to automatically generate hardware assertion checkers, used to monitor assertions during simulation or emulation. Another challenge is ABV for SoC (systems on chip) modeled at the Electronic System Level (ESL). One of the ESL flagship languages is the IEEE standard 1666 SystemC, with its Transactional Level Modeling (TLM) support. SystemC TLM enables the description of virtual platforms that serve as golden models. At this level of abstraction, where integration testing is a major issue, requirements to be verified usually express temporal constraints on the interactions and communications between hardware/software components of the SoC.
This talk will present the major steps of the design flow, the characteristics of temporal assertions emblematic of System and RT levels, respective issues related to their monitoring, and our solutions to automatically generate assertion checkers and instrument IP or system descriptions for runtime verification.

César Sanchez (IMDEA Madrid, Spain) – slides slides

 Stream Runtime Verification

Stream Runtime Verification is behavioral specification language for runtime verification, where a monitor is described by expressing the dependencies between the output streams of values in terms of the input streams of observations.

The classical approaches to runtime verification borrow specification languages from static verification, like linear temporal logic (LTL), LTL for finite traces, regular expressions, etc. In comparison, stream runtime verification is based on the observation that many monitoring algorithms can be generalized from Booleans to rich data domains. Stream runtime verification provides a friendly language (with a programming look and feel) to express these dependencies and automatically generate monitors that compute streams of values from streams of observations. At the same time, one can translate automatically logical specifications into stream runtime verification specifications with a correctness guarantee.

In this lecture I will introduce runtime verification, the monitorable and efficiently monitorable fragments, and show online and offline algorithms. In the second part I will present some extensions of stream runtime verification, for example to handle parametrized data and real-time event streams.

Gerardo Schneider (Chalmers University of Technology, Sweden) – slides

Monitoring Data Minimization

In this talk I will consider the runtime verification problem of safety hyperproperties for deterministic programs. Several security and information-flow policies such as data minimality, non-interference, integrity, and software doping are naturally expressed formally as safety hyperproperties. Although there are monitoring results for hyperproperties, the algorithms are very complex since these are properties over set of traces, and not over single traces. For the deterministic input-output programs that we consider, and the specific safety hyperproperties we are interested in, the problem can be reduced to monitoring of trace properties. I will present a simple monitoring approach for safety hyperproperties of deterministic programs, focusing in particular in data minimization. The approach involves transforming the given safety hyperproperty into a trace property,  extracting a characteristic predicate for the given hyperproperty, and providing a parametric monitor taking such predicate as parameter. For any hyperproperty in the considered subclass, we show how runtime verification monitors can be synthesized. I will discuss results concerning both offline and online monitoring of such kind of properties.