Skip to main content

Über dieses Buch

This book constitutes the refereed proceedings of the 5th International Conference on Runtime Verification, RV 2014, held in Toronto, ON, Canada in September 2014. The 28 revised full papers presented together with 2 tool papers, and 8short papers were carefully reviewed and selected from 70 submissions. The scope of the conference was on following topics: monitoring and trace slicing, runtime verification of distributed and concurrent systems, runtime Verification of real-time and embedded systems, testing and bug finding, and inference and learning.



First International Competition on Software for Runtime Verification

We report on the process of organizing the First International Competition on Software for Runtime Verification (CSRV). The report describes the format, participating teams and evaluation process. The competition was held as a satellite event of the 14th International Conference on Runtime Verification (RV’14). The Competition was organized in three tracks: offline monitoring, online monitoring of C programs, and online monitoring of Java programs.
Ezio Bartocci, Borzoo Bonakdarpour, Yliès Falcone

Monitoring and Trace Slicing

Multiple Ways to Fail: Generalizing a Monitor’s Verdict for the Classification of Execution Traces

This paper introduces a new approach at classifying event traces, generalizing a monitor’s classical two- or three-valued outcome. Given the specification of a system’s behaviour expressed as a Linear Temporal Logic formula, we produce from the evaluation of the formula on a given trace a data structure called a trace hologram. When interpreted as equivalence classes, we show how manipulations on these holograms cluster event traces into various natural categories, depending on the precise way in which each group of traces violate the specification.
Simon Varvaressos, Kim Lavoie, Sébastien Gaboury, Sylvain Hallé

Two Generalisations of Roşu and Chen’s Trace Slicing Algorithm A

Roşu and Chen’s trace analysis algorithm identifies activity streams in a monitored application based on data (such as memory locations) and groups events accordingly into slices. It can be generalised to assign several such activity streams to the same slice, even if data is unrelated. This is useful for monitoring scheduling algorithms, which linearise activity streams that are not necessarily related. The algorithm can be generalised further to impose constraints on the generated slices such that, for example, each trace relates a high-priority activity to a low-priority activity. There are no limitations on constraints other than that constraint solvers efficient enough for runtime analysis need to be available.
Clemens Ballarin

Scalable Offline Monitoring

We propose an approach to monitoring IT systems offline, where system actions are logged in a distributed file system and subsequently checked for compliance against policies formulated in an expressive temporal logic. The novelty of our approach is that monitoring is parallelized so that it scales to large logs. Our technical contributions comprise a formal framework for slicing logs, an algorithmic realization based on MapReduce, and a high-performance implementation. We evaluate our approach analytically and experimentally, proving the soundness and completeness of our slicing techniques and demonstrating its practical feasibility and efficiency on real-world logs with 400 GB of relevant data.
David Basin, Germano Caronni, Sarah Ereth, Matúš Harvan, Felix Klaedtke, Heiko Mantel

Monitoring Systems with Extended Live Sequence Charts

A problem with most runtime verification techniques is that the monitoring specification formalisms are often complex. In this paper, we propose an extension of live sequence charts (LSCs) which avoids this problem. We extend the standard LSCs as proposed by Damm and Harel by introducing the notion of “sufficient prechart”, and by adding concatenation and iteration of charts. With these extended LSCs, necessary and sufficient conditions of certain statements can be intuitively specified. Moreover, similar as for message sequence charts, sequencing and iteration allow to express multiple scenarios. We give a translation of extended LSCs into linear temporal logic formulae, and develop online monitoring algorithms for traces with respect to extended LSCs. We use our algorithm to test a concrete example from the European Train Control System (ETCS) standard, and evaluate it on several benchmarks. The results show the feasibility of our approach.
Ming Chai, Bernd-Holger Schlingloff

Foundations of Boolean Stream Runtime Verification

Stream runtime verification (SRV), pioneered by the tool LOLA, is a declarative approach to specify synchronous monitors. In SRV, monitors are described by specifying dependencies between output streams of values and input streams of values. The declarative nature of SRV enables a separation between (1) the evaluation algorithms, and (2) the monitor storage and its individual updates. This separation allows SRV to be lifted from conventional failure monitors into richer domains to collect statistics of traces. Moreover, SRV allows to easily identify specifications that can be efficiently monitored online, and to generate efficient schedules for offline monitors.
In spite of these attractive features, many important theoretical problems about SRV are still open. In this paper, we address complexity, expressiveness, succinctness, and closure issues for the subclass of Boolean SRV (BSRV) specifications. Additionally, we show that for this subclass, offline monitoring can be performed with only two passes (one forward and one backward) over the input trace in spite of the alternation of past and future references in the BSRV specification.
Laura Bozzelli, César Sánchez

Portable Runtime Verification with Smartphones and Optical Codes

We describe a prototype architecture for the runtime monitoring of Java programs using a smartphone. An online tool can produce an AspectJ file which, when woven with the program to be monitored and executed, instantiates a GUI window where XML events from the program’s execution are output in the form of QR codes. We illustrate the feasibility of this approach by monitoring runtime properties on the execution of a video game by pointing a handheld Android phone at the game’s screen and obtaining realtime feedback.
Kim Lavoie, Corentin Leplongeon, Simon Varvaressos, Sébastien Gaboury, Sylvain Hallé

Robust Consistency Checking for Modern Filesystems

We describe our approach to building a runtime file system checker for the emerging Linux Btrfs file system. Such checkers verify the consistency of file system metadata update operations before they are committed to disk, thus preventing corrupted updates from becoming durable. The consistency checks in Btrfs are complex and need to be expressed clearly so that they can be reasoned about and implemented reliably, thus we propose writing the checks declaratively. This approach reduces the complexity of the checks, ensures their independence, and helps identify the correct abstractions in the checker. It also shows how the checker can be made robust against arbitrary file system corruption.
Kuei Sun, Daniel Fryer, Dai Qin, Angela Demke Brown, Ashvin Goel

Runtime Verification of Distributed and Concurrent Systems

On the Number of Opinions Needed for Fault-Tolerant Run-Time Monitoring in Distributed Systems

Decentralized runtime monitoring involves a set of monitors observing the behavior of system executions with respect to some correctness property. It is generally assumed that, as soon as a violation of the property is revealed by any of the monitors at runtime, some recovery code can be executed for bringing the system back to a legal state. This implicitly assumes that each monitor produces a binary opinion, true or false, and that the recovery code is launched as soon as one of these opinions is equal to false. In this paper, we formally prove that, in a failure-prone asynchronous computing model, there are correctness properties for which there is no such decentralized monitoring. We show that there exist some properties which, in order to be monitored in a wait-free decentralized manner, inherently require that the monitors produce a number of opinions larger than two. More specifically, our main result is that, for every k, 1 ≤ k ≤ n, there exists a property that requires at least k opinions to be monitored by n monitors. We also present a corresponding distributed monitor using at most k + 1 opinions, showing that our lower bound is nearly tight.
Pierre Fraigniaud, Sergio Rajsbaum, Corentin Travers

Supporting the Specification and Runtime Validation of Asynchronous Calling Patterns in Reactive Systems

Wireless sensor networks (“sensornets”) are highly distributed and concurrent, with program actions bound to external stimuli. They exemplify a system class known as reactive systems, which comprise execution units that have “hidden” layers of control flow. A key obstacle in enabling reactive system developers to rigorously validate their implementations has been the absence of precise software component specifications and tools to assist in leveraging those specifications at runtime. We address this obstacle in three ways: (i) We describe a specification approach tailored for reactive environments and demonstrate its application in the context of sensornets. (ii) We describe the design and implementation of extensions to the popular nesC tool-chain that enable the expression of these specifications and automate the generation of runtime monitors that signal violations, if any. (iii) Finally, we apply the specification approach to a significant collection of the most commonly used software components in the TinyOS distribution and analyze the overhead involved in monitoring their correctness.
Jiannan Zhai, Nigamanth Sridhar, Jason O. Hallstrom

Speculative Program Parallelization with Scalable and Decentralized Runtime Verification

Thread Level Speculation (TLS) is a dynamic code parallelization technique proposed to keep the software in pace with the advances in hardware, in particular, to automatically parallelize programs to take advantage of the multi-core processors. Being speculative, frameworks of this type unavoidably rely on verification systems that are similar to software transactional memory, and that require voluminous inter-thread communications or centralized registering of the performed memory accesses. The high degree of communication is against the basic principles of high performance parallel computing, does not scale with an increasing number of processor cores, and yields weak performance. Moreover, TLS systems often apply one unique parallelization strategy consisting in slicing a loop into several parallel speculative threads. Such a strategy is also against the basic principles since loops in the original serial code are not necessarily parallel and also, it is well-known that the parallel schedule must promote data locality which is crucial in obtaining good performance. This situation appeals to scalable and decentralized verification systems and new strategies to dynamically generate efficient parallel code resulting from advanced optimizing parallelizing transformations. Such transformations require a more complex verification system that allows intra-thread iterations to be reordered. In this paper, we propose a verification system of this kind, based on a model built at runtime and predicting a linear memory behavior. This strategy is part of the Apollo speculative code parallelizer which is based on an adaptation for dynamic usage of the polyhedral model.
Aravind Sukumaran-Rajam, Juan Manuel Martinez Caamaño, Willy Wolff, Alexandra Jimborean, Philippe Clauss

Organising LTL Monitors over Distributed Systems with a Global Clock

Users wanting to monitor distributed systems often prefer to abstract away the architecture of the system, allowing them to directly specify correctness properties on the global system behaviour. To support this abstraction, a compilation of the properties would not only involve the typical choice of monitoring algorithm, but also the organisation of submonitors across the component network. Existing approaches, considered in the context of LTL properties over distributed systems with a global clock, include the so-called orchestration and migration approaches. In the orchestration approach, a central monitor receives the events from all subsystems. In the migration approach, LTL formulae transfer themselves across subsystems to gather local information.
We propose a third way of organising submonitors: choreography — where monitors are orgnized as a tree across the distributed system, and each child feeds intermediate results to its parent. We formalise this approach, proving its correctness and worst case performance, and report on an empirical investigation comparing the three approaches on several concerns of decentralised monitoring.
Christian Colombo, Yliès Falcone

Dynamic Verification for Hybrid Concurrent Programming Models

We present a dynamic verification technique for a class of concurrent programming models that combine dataflow and shared memory programming. In this class of hybrid concurrency models, programs are built from tasks whose data dependencies are explicitly defined by a programmer and used by the runtime system to coordinate task execution. Differently from pure dataflow, tasks are allowed to have shared state which must be properly protected using synchronization mechanisms, such as locks or transactional memory (TM). While these hybrid models enable programmers to reason about programs, especially with irregular data sharing and communication patterns, at a higher level, they may also give rise to new kinds of bugs as they are unfamiliar to the programmers. We identify and illustrate a novel category of bugs in these hybrid concurrency programming models and provide a technique for randomized exploration of program behaviors in this setting.
Erdal Mutlu, Vladimir Gajinov, Adrián Cristal, Serdar Tasiran, Osman S. Unsal

Abstraction and Mining of Traces to Explain Concurrency Bugs

We propose an automated mining-based method for explaining concurrency bugs. We use a data mining technique called sequential pattern mining to identify problematic sequences of concurrent read and write accesses to the shared memory of a multi-threaded program. Our technique does not rely on any characteristics specific to one type of concurrency bug, thus providing a general framework for concurrency bug explanation. In our method, given a set of concurrent execution traces, we first mine sequences that frequently occur in failing traces and then rank them based on the number of their occurrences in passing traces. We consider the highly ranked sequences of events that occur frequently only in failing traces an explanation of the system failure, as they can reveal its causes in the execution traces. Since the scalability of sequential pattern mining is limited by the length of the traces, we present an abstraction technique which shortens the traces at the cost of introducing spurious explanations. Spurious as well as misleading explanations are then eliminated by a subsequent filtering step, helping the programmer to focus on likely causes of the failure. We validate our approach using a number of case studies, including synthetic as well as real-world bugs.
Mitra Tabaei Befrouei, Chao Wang, Georg Weissenbacher

Runtime Verification of Real-Time and Embedded Systems

Online Monitoring of Metric Temporal Logic

Current approaches to monitoring real-time properties suffer either from unbounded space requirements or lack of expressiveness. In this paper, we adapt a separation technique enabling us to rewrite arbitrary MTL formulas into LTL formulas over a set of atoms comprising bounded MTL formulas. As a result, we obtain the first trace-length independent online monitoring procedure for full MTL in a dense-time setting.
Hsi-Ming Ho, Joël Ouaknine, James Worrell

On Real-Time Monitoring with Imprecise Timestamps

Existing real-time monitoring approaches assume traces with precise timestamps. Their correctness is thus indefinite when monitoring the behavior of systems with imprecise clocks. We address this problem for a metric temporal logic: We identify classes of formulas for which we can leverage existing monitors to correctly reason about observed system traces.
David Basin, Felix Klaedtke, Srdjan Marinovic, Eugen Zălinescu

ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models

Formal verification and validation play a crucial role in making cyber-physical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified w.r.t. the model. Otherwise, all bets are off. This paper introduces ModelPlex, a method ensuring that verification results about models apply to CPS implementations. ModelPlex provides correctness guarantees for CPS executions at runtime: it combines offline verification of CPS models with runtime validation of system executions for compliance with the model. ModelPlex ensures that the verification results obtained for the model apply to the actual system runs by monitoring the behavior of the world for compliance with the model, assuming the system dynamics deviation is bounded. If, at some point, the observed behavior no longer complies with the model so that offline verification results no longer apply, ModelPlex initiates provably safe fallback actions. This paper, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic.
Stefan Mitsch, André Platzer

Runtime Observer Pairs and Bayesian Network Reasoners On-board FPGAs: Flight-Certifiable System Health Management for Embedded Systems

Safety-critical systems, like Unmanned Aerial Systems (UAS) that must operate totally autonomously, e.g., to support ground-based emergency services, must also provide assurance they will not endanger human life or property in the air or on the ground. Previously, a theoretical construction for paired synchronous and asynchronous runtime observers with Bayesian reasoning was introduced that demonstrated the ability to handle runtime assurance within the strict operational constraints to which the system must adhere. In this paper, we show how to instantiate and implement temporal logic runtime observers and Bayesian network diagnostic reasoners that use the observers’ outputs, on-board a field-standard Field Programmable Gate Array (FPGA) in a way that satisfies the strict flight operational standards of Realizability, Responsiveness, and Unobtrusiveness. With this type of compositionally constructed diagnostics framework we can develop compact, hierarchical, and highly expressive health management models for efficient, on-board fault detection and system monitoring. We describe an instantiation of our System Health Management (SHM) framework, rt-R2U2, on standard FPGA hardware, which is suitable to be deployed on-board a UAS. We run our system with a full set of real flight data from NASA’s Swift UAS, and highlight a case where our runtime SHM framework would have been able to detect and diagnose a fault from subtle evidence that initially eluded traditional real-time diagnosis procedures.
Johannes Geist, Kristin Y. Rozier, Johann Schumann

On-Line Monitoring for Temporal Logic Robustness

In this paper, we provide a Dynamic Programming algorithm for on-line monitoring of the state robustness of Metric Temporal Logic specifications with past time operators. We compute the robustness of MTL with unbounded past and bounded future temporal operators (MTL\(^{<+\infty}_{+pt}\)) over sampled traces of Cyber-Physical Systems. We implemented our tool in Matlab as a Simulink block that can be used in any Simulink model. We experimentally demonstrate that the overhead of the MTL\(^{<+\infty}_{+pt}\) robustness monitoring is acceptable for certain classes of practical specifications.
Adel Dokhanchi, Bardh Hoxha, Georgios Fainekos

ROSRV: Runtime Verification for Robots

We present ROSRV, a runtime verification framework for robotic applications on top of the Robot Operating System (ROS [8]), a widely used open-source framework for robot software development. ROSRV aims to address the safety and security issues of robots by providing a transparent monitoring infrastructure that intercepts and monitors the commands and messages passing through the system. Safety and security properties can be defined in a formal specification language, and are ensured by automatically generated monitors. ROSRV integrates seamlessly with ROS—no change in ROS nor the application code is needed. ROSRV has been applied and evaluated on a commercial robot.
Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon Moore, Qingzhou Luo, Aravind Sundaresan, Grigore Rosu

Testing and Bug Finding

Symbolic Execution Debugger (SED)

We present the Symbolic Execution Debugger for sequential Java programs. Being based on symbolic execution, its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all program execution paths are explored simultaneously. To support program comprehension, execution paths as well as intermediate states are visualized.
Martin Hentschel, Richard Bubel, Reiner Hähnle

Checking Data Structure Properties Orders of Magnitude Faster

Executable formal contracts help verify a program at runtime when static verification fails. However, these contracts may be prohibitively slow to execute, especially when they describe the transformations of data structures. In fact, often an efficient data structure operation with O(log(n)) running time executes in O(n log(n)) when naturally written specifications are executed at run time.
We present a set of techniques that improve the efficiency of run-time checks by orders of magnitude, often recovering the original asymptotic behavior of operations. Our implementation first removes any statically verified parts of checks. Then, it applies a program transformation that changes recursively computed properties into data structure fields, ensuring that properties are evaluated no more than once on a given data structure node. We present evaluation of our techniques on the Leon system for verification of purely functional programs.
Emmanouil Koukoutos, Viktor Kuncak

Dynamic Test Generation with Static Fields and Initializers

Static state is common in object-oriented programs. However, automatic test case generators do not take into account the potential interference of static state with a unit under test and may, thus, miss subtle errors. In particular, existing test case generators do not treat static fields as input to the unit under test and do not control the execution of static initializers. We address these issues by presenting a novel technique in automatic test case generation based on static analysis and dynamic symbolic execution. We have applied this technique on a suite of open-source applications and found errors that go undetected by existing test case generators. Our experiments show that this problem is relevant in real code, indicate which kinds of errors existing techniques miss, and demonstrate the effectiveness of our technique.
Maria Christakis, Patrick Emmisberger, Peter Müller

RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties

Runtime verification can effectively increase the reliability of software systems. In recent years, parametric runtime verification has gained a lot of traction, with several systems proposed. However, lack of real specifications and prohibitive runtime overhead when checking numerous properties simultaneously prevent developers or users from using runtime verification. This paper reports on more than 150 formal specifications manually derived from the Java API documentation of commonly used packages, as well as a series of novel techniques which resulted in a new runtime verification system, RV-Monitor. Experiments show that these specifications are useful for finding bugs and bad software practice, and RV-Monitor is capable of monitoring all our specifications simultaneously, and runs substantially faster than other state-of-the-art runtime verification systems.
Qingzhou Luo, Yi Zhang, Choonghwan Lee, Dongyun Jin, Patrick O’Neil Meredith, Traian Florin Şerbănuţă, Grigore Roşu

Inference and Learning

Improving Dynamic Inference with Variable Dependence Graph

Dynamic detection of program invariants infers relationship between variables at program points using trace data, but reports a large number of irrelevant invariants. We outline an approach that combines lightweight static analysis with dynamic inference that restricts irrelevant comparisons. This is achieved by constructing a variable dependence graph relating a procedure’s input and output variables. Initial experiments indicate the advantage of this approach over the dynamic analysis tool Daikon.
Anand Yeolekar

The TTT Algorithm: A Redundancy-Free Approach to Active Automata Learning

In this paper we present TTT, a novel active automata learning algorithm formulated in the Minimally Adequate Teacher (MAT) framework. The distinguishing characteristic of TTT is its redundancy-free organization of observations, which can be exploited to achieve optimal (linear) space complexity. This is thanks to a thorough analysis of counterexamples, extracting and storing only the essential refining information. TTT is therefore particularly well-suited for application in a runtime verification context, where counterexamples (obtained, e.g., via monitoring) may be excessively long: as the execution time of a test sequence typically grows with its length, this would otherwise cause severe performance degradation. We illustrate the impact of TTT’s consequent redundancy-free approach along a number of examples.
Malte Isberner, Falk Howar, Bernhard Steffen

Lazy Symbolic Execution for Enhanced Learning

The performance of symbolic execution based verifiers relies heavily on the quality of “interpolants”, formulas which succinctly describe a generalization of states proven safe so far. By default, symbolic execution along a path stops the moment when infeasibility is detected in its path constraints, a property we call “eagerness”. In this paper, we argue that eagerness may hinder the discovery of good quality interpolants, and propose a systematic method that ignores the infeasibility in pursuit of better interpolants. We demonstrate with a state-of-the-art system on realistic benchmarks that this “lazy” symbolic execution outperforms its eager counterpart by a factor of two or more.
Duc-Hiep Chu, Joxan Jaffar, Vijayaraghavan Murali

Faster Statistical Model Checking by Means of Abstraction and Learning

This paper investigates the combined use of abstraction and probabilistic learning as a means to enhance statistical model checking performance. We are given a property (or a list of properties) for verification on a (large) stochastic system. We project on a set of traces generated from the original system, and learn a (small) abstract model from the projected traces, which contain only those labels that are relevant to the property to be verified. Then, we model-check the property on the reduced, abstract model instead of the large, original system. In this paper, we propose a formal definition of the projection on traces given a property to verify. We also provide conditions ensuring the correct preservation of the property on the abstract model. We validate our approach on the Herman’s Self Stabilizing protocol. Our experimental results show that (a) the size of the abstract model and the verification time are drastically reduced, and that (b) the probability of satisfaction of the property being verified is correctly estimated by statistical model checking on the abstract model with respect to the concrete system.
Ayoub Nouri, Balaji Raman, Marius Bozga, Axel Legay, Saddek Bensalem


Weitere Informationen

Premium Partner