Online and Offline Stream Runtime Verification of Synchronous Systems
Cesar Sanchez, IMDEA Software Institute, Madrid
Abstract: We revisit Stream Runtime Verification (SRV) for synchronous systems. Stream runtime verification is a formalism to express monitors using streams, which results in a simple and expressive specification language that can describe both correctness/failure assertions along with interesting statistical measures for system profiling and coverage analysis. The monitors generated are useful for testing, under actual deployment, and to analyze logs.
The key idea of Stream Runtime Verification is the observation that the steps in the algorithms to monitor logics (which generate Boolean verdicts) can be generalized to compute statistics of the trace if a different data domain is used. Hence, the core of SRV is to separate the temporal dependencies in the monitoring algorithm with the concrete operations to be performed at each step. We revisit the pioneer SRV specification language Lola and study online and offline monitoring algorithms.
The algorithm for online monitoring Lola specifications uses a partial evaluation strategy, by incrementally constructing output streams from input streams, maintaining a store of partially evaluated expressions. We identify syntactically a class of specifications for which the online algorithm is trace length independent, that is, the memory requirement does not depend on the length of the input streams. Then, we extend the principles of the online algorithm to create an efficient offline monitoring algorithm for large traces, which consist on scheduling trace length independent passes on a dumped log.
Monitoring Smart Contracts: ContractLarva and Open Challenges Beyond
Shaun Azzopardi, Joshua Ellul and Gordon J. Pace
Abstract: Smart contracts present new challenges for runtime verification techniques, due to features such as immutability of the code once enacted, the notion of gas that must be paid for the execution of code, and the possibility for a transaction to fail and have no effect. In this tutorial we present the runtime verification tool ContractLarva and outline its use in instrumenting monitors in smart contracts written in Solidity for the Ethereum blockchain-based distributed computing platform. We discuss the challenges faced in doing so, and how some of these are addressed, using the ERC-20 token standard to illustrate this. We conclude by proposing a list of open challenges in smart contract and blockchain monitoring.
Can We Monitor Multi-threaded Java Programs?
Ylies Falcone, Université Grenoble Alpes
Antoine El-Hokayem, Université Grenoble Alpes
Abstract: Runtime Verification (RV) is a lightweight formal method which consists in verifying that an execution of a program is correct wrt. a specification. The specification formalizes with properties the expected correct behavior of the system. Programs are instrumented to extract necessary information from the execution and feed it to monitors tasked with checking the properties. From the perspective of a monitor, the system is a black box; the trace is the only system information provided. Parallel programs generally introduce an added level of complexity on the program execution due to concurrency. A concurrent execution of a parallel program is best represented as a partial order. A large number of RV approaches generate monitors using formalisms that rely on total order, while more recent approaches utilize formalisms that consider multiple traces.
In this tutorial, we review some of the main RV approaches and tools that handle multithreaded Java programs. We discuss their assumptions, limitations, expressiveness, and suitability when tackling parallel programs such as producer-consumer and readers-writers. By analyzing the interplay between specification formalisms and concurrent executions of programs, we identify four questions RV practitioners may ask themselves to classify and determine the situations in which it is sound to use the existing tools and approaches.
Hardware-based Runtime Verification with Embedded Tracing Units and Stream Processing
Lukas Convent, Sebastian Hungerecker, Torben Scheffel, Malte Schmitz, Daniel Thoma, Alexander Weiss
Abstract: In this tutorial, we present a comprehensive approach to non-intrusive monitoring of multi-core processors. Modern multi-core processors come with trace-ports that provide a highly compressed trace of the instructions executed by the processor. We describe how these traces can be used to reconstruct the control flow of a program running on the processor and to carry out analyses on the control flow in real time using FPGAs. We further give an introduction to the temporal stream-based specification language TeSSLa and show how it can be used to specify typical constraints of a cyber-physical system from the railway domain. Finally, we describe how light-weight, hardware-supported instrumentation can be used to enrich the control-flow trace with data values from the application.
This work is supported in part by the European COST Action ARVI, the BMBF project ARAMiS II with funding ID 01 IS 16025, and the European Horizon 2020 project COEMS under number 732016.
Runtime Verification – From Propositional to First-Order Temporal Logic
Klaus Havelund and Doron Peled
Abstract: Runtime Verification is a subfield of formal methods concerned with analysis of execution traces for the purpose of determining the state or general quality of the executing system. The field covers numerous approaches, one of which is specification-based runtime verification, where execution traces are checked against formal specifications. Specifications can be written in a number of different logics, including e.g. temporal logics, state machines, and regular expressions. In this tutorial we shall specifically focus on future and past time temporal logics.
We first present propositional temporal logics, where observed events in the execution trace are atomic propositions. We present their semantics and some monitoring algorithms for past time temporal logic based on dynamic programming, and for future time temporal logic based on automata.
We subsequently more generally discuss monitorability of temporal properties by dividing them into different classes representing different degrees of monitorability, and we provide algorithms for classifying properties according to these classes.
We then present first-order temporal logic and its semantics. First-order temporal logic contains quantifiers, allowing to quantify over data occurring as arguments in observed events. Monitoring of the first-order case is drastically more challenging than the propositional case, since it requires efficiently storing and searching the data values observed in traces that are potentially unbounded. We present a new solution to this problem using BDDs (Binary Decision Diagrams). We first introduce BDDs, and subsequently we demonstrate their use in a monitoring algorithm based on the dynamic programming algorithm used for the past time propositional case introduced earlier.
Monitoring, Learning and Control of Cyber-Physical Systems with STL (Tutorial)
Abstract: Signal Temporal Logic (STL) is a popular specification language to reason about continuous-time trajectories of dynamical systems. STL was originally employed to specify and to monitor requirements over the evolution of physical quantities and discrete states characterizing the behavior of cyber-physical systems (CPS).
More recently, this formalism plays a key role in several approaches for the automatic design of safe systems and controllers satisfying an STL specification. However, requirements for CPS may include behavioral properties about the physical plant that are not always fully known a-priori and indeed cannot be manually specified. This has opened also new research direction on efficient methods for automatically mining and learning STL properties from data measurements.
In this tutorial we provide an overview of the state-of-the-art approaches available for monitoring, learning and control of CPS behaviors focusing on some recent applications.