Skip to main content
main-content

Über dieses Buch

This book constitutes the refereed proceedings of the 6th International Conference on Runtime Verification, RV 2015, held in Vienna, Austria, in September 2015. The 15 revised full papers presented together with 4 short papers, 2 tool papers, 4 tutorials, 3 invited talks, and 2 software competition papers were carefully reviewed and selected from 45 submissions.
The discussion of the conference centers around two main aspects. The first is to understand wether the runtime verification techniques can practically complement the traditional methods proving programs correct before their execution, such as model checking and theorem proving. The second concerns with formal methods and how their application can improve traditional ad-hoc monitoring techniques used in performance monitoring, hardware design emulation and simulation, etc.

Inhaltsverzeichnis

Frontmatter

Invited Paper

Frontmatter

Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification

Abstract
In this paper, we briefly examine the recent developments in artificial pancreas controllers, that automate the delivery of insulin to patients with type-1 diabetes. We argue the need for offline and online runtime verification for these devices, and discuss challenges that make verification hard. Next, we examine a promising simulation-based falsification approach based on robustness semantics of temporal logics. These ideas are implemented in the tool S-Taliro that automatically searches for violations of metric temporal logic (MTL) requirements for Simulink(tm)/Stateflow(tm) models. We illustrate the use of S-Taliro for finding interesting property violations in a PID-based hybrid closed loop control system.
Fraser Cameron, Georgios Fainekos, David M. Maahs, Sriram Sankaranarayanan

Regular Papers

Frontmatter

Qualitative and Quantitative Monitoring of Spatio-Temporal Properties

Abstract
We address the specification and verification of spatio-temporal behaviours of complex systems, extending Signal Spatio-Temporal Logic (SSTL) with a spatial operator capable of specifying topological properties in a discrete space. The latter is modelled as a weighted graph, and provided with a boolean and a quantitative semantics. Furthermore, we define efficient monitoring algorithms for both the boolean and the quantitative semantics. These are implemented in a Java tool available online. We illustrate the expressiveness of SSTL and the effectiveness of the monitoring procedures on the formation of patterns in a Turing reaction-diffusion system.
Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, Mieke Massink

Runtime Adaptation for Actor Systems

Abstract
We study the problem of extending RV techniques in the context of (asynchronous) actor systems, so as to be able to carry out a degree of system adaptation at runtime. We propose extensions to specification logics that provide handles for programming both monitor synchronisations (with individual actors), as well as the administration of the resp. adaptations once the triggering behaviour is observed. Since this added functionality allows the specifier to introduce erroneous adaptation procedures, we also develop static analysis techniques based on substructural type systems to assist the construction of correct adaptation scripts.
Ian Cassar, Adrian Francalanza

Robust Online Monitoring of Signal Temporal Logic

Abstract
Requirements of cyberphysical systems (CPS) can be rigorously specified using Signal Temporal Logic (STL). STL comes equipped with semantics that are able to quantify how robustly a given signal satisfies an STL property. In a setting where signal values over the entire time horizon of interest are available, efficient algorithms for offline computation of the robust satisfaction value have been proposed. Only a few methods exist for the online setting, i.e., where only a partial signal trace is available and rest of the signal becomes available in increments (such as in a real system or during numerical simulations). In this paper, we formalize the semantics for robust online monitoring of partial signals using the notion of robust satisfaction intervals (\(\mathtt {RoSI}\)s). We propose an efficient algorithm to compute the \(\mathtt {RoSI}\) and demonstrate its usage on two real-world case studies from the automotive domain and massively-online CPS education. As online algorithms permit early termination when the satisfaction or violation of a property is found, we show that savings in computationally expensive simulations far outweigh any overheads incurred by the online approach.
Jyotirmoy V. Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, Sanjit A. Seshia

On Verifying Hennessy-Milner Logic with Recursion at Runtime

Abstract
We study \(\mu \) HML (a branching-time logic with least and greatest fixpoints) from a runtime verification perspective. We establish which subset of the logic can be verified at runtime and define correct monitor-synthesis algorithms for this subset. We also prove completeness results https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23820-3_5/367589_1_En_5_IEq2_HTML.gif these logical subsets that show that no other properties apart from those identified can be verified at runtime.
Adrian Francalanza, Luca Aceto, Anna Ingolfsdottir

Assuring the Guardians

Abstract
Ultra-critical systems are growing more complex, and future systems are likely to be autonomous and cannot be assured by traditional means. Runtime Verification (RV) can act as the last line of defense to protect the public safety, but only if the RV system itself is trusted. In this paper, we describe a model-checking framework for runtime monitors. This tool is integrated into the Copilot language and framework aimed at RV of ultra-critical hard real-time systems. In addition to describing its implementation, we illustrate its application on a number of examples ranging from very simple to the Boyer-Moore majority vote algorithm.
Jonathan Laurent, Alwyn Goodloe, Lee Pike

A Case Study on Runtime Monitoring of an Autonomous Research Vehicle (ARV) System

Abstract
Runtime monitoring is a versatile technique for detecting property violations in safety-critical (SC) systems. Although instrumentation of the system under monitoring is a common approach for obtaining the events relevant for checking the desired properties, the current trend of using black-box commercial-off-the-shelf components in SC system development makes these systems unamenable to instrumentation. In this paper we develop an online runtime monitoring approach targeting an autonomous research vehicle (ARV) system and recount our experience with it. To avoid instrumentation we passively monitor the target system by generating atomic propositions from the observed network state. We then develop an efficient runtime monitoring algorithm, EgMon, that eagerly checks for violations of desired properties written in future-bounded, propositional metric temporal logic. We show the efficacy of EgMon by implementing and empirically evaluating it against logs obtained from the testing of an ARV system. EgMon was able to detect violations of several safety requirements.
Aaron Kane, Omar Chowdhury, Anupam Datta, Philip Koopman

Monitoring Electronic Exams

Abstract
Universities and other educational organizations are adopting computer-based assessment tools (herein called e-exams) to reach larger and ubiquitous audiences. While this makes examination tests more accessible, it exposes them to unprecedented threats not only from candidates but also from authorities, which organize exams and deliver marks. Thus, e-exams must be checked to detect potential irregularities. In this paper, we propose several monitors, expressed as Quantified Event Automata (QEA), to monitor the main properties of e-exams. Then, we implement the monitors using MarQ, a recent Java tool designed to support QEAs. Finally, we apply our monitors to logged data from real e-exams conducted by Université Joseph Fourier at pharmacy faculty, as a part of Epreuves Classantes Nationales informatisées, a pioneering project which aims to realize all french medicine exams electronically by 2016. Our monitors found discrepancies between the specification and the implementation.
Ali Kassem, Yliès Falcone, Pascal Lafourcade

Monitoring Real Android Malware

Abstract
In the most comprehensive study on Android attacks so far (undertaken by the Android Malware Genome Project), the behaviour of more than 1, 200 malwares was analysed and categorised into common, recurring groups of attacks. Based on this work (and the corresponding actual malware files), we present an approach for specifying and identifying these (and similar) attacks using runtime verification.
While formally, our approach is based on a first-order logic abstraction of malware behaviour, it practically relies on our Android event interception tool, MonitorMe, which lets us capture almost any system event that can be triggered by apps on a user’s Android device.
This paper details on MonitorMe, our formal specification of malware behaviour and practical experiments, undertaken with various different Android devices and versions on a wide range of actual malware incarnations from the above study. In a nutshell, we were able to detect real malwares from 46 out of 49 different malware families, which strengthen the idea that runtime verification may, indeed, be a good choice for mobile security in the future.
Jan-Christoph Küster, Andreas Bauer

Time-Triggered Runtime Verification of Component-Based Multi-core Systems

Abstract
In this paper, we characterize and solve the problem of augmenting a component-based system with time-triggered runtime verification (TTRV), where different components are expected to run on different computing cores with minimum monitoring overhead at run time. We present an optimization technique that calculates (1) the mapping of components to computing cores, and (2) the monitoring frequency, such that TTRV’s runtime overhead is minimized. Although dealing with runtime overhead of concurrent systems is a challenging problem due to their inherent complex nature, our experiments show that our optimization technique is robust and reduces the monitoring overhead by 34 %, as compared to various near-optimal monitoring patterns of the components at run time.
Samaneh Navabpour, Borzoo Bonakdarpour, Sebastian Fischmeister

Monitoring for a Decidable Fragment of MTL- $\int$

Abstract
Temporal logics targeting real-time systems are traditionally undecidable. Based on a restricted fragment of MTL-\(\int \), we propose a new approach for the runtime verification of hard real-time systems. The novelty of our technique is that it is based on incremental evaluation, allowing us to effectively treat duration properties (which play a crucial role in real-time systems). We describe the two levels of operation of our approach: offline simplification by quantifier removal techniques; and online evaluation of a three-valued interpretation for formulas of our fragment. Our experiments show the applicability of this mechanism as well as the validity of the provided complexity results.
André de Matos Pedro, David Pereira, Luís Miguel Pinho, Jorge Sousa Pinto

Runtime Verification Through Forward Chaining

Abstract
In this paper we present a novel rule-based approach for Runtime Verification of FLTL properties over finite but expanding traces. Our system exploits Horn clauses in implication form and relies on a forward chaining-based monitoring algorithm. This approach avoids the branching structure and exponential complexity typical of tableaux-based formulations, creating monitors with a single state and a fixed number of rules. This allows for a fast and scalable tool for Runtime Verification: we present the technical details together with a working implementation.
Alan Perotti, Guido Boella, Artur d’Avila Garcez

Collision Avoidance for Mobile Robots with Limited Sensing and Limited Information About the Environment

Abstract
This paper addresses the problem of safely navigating a mobile robot with limited sensing capability and limited information about stationary obstacles. We consider two sensing limitations: blind spots between sensors and limited sensing range. We identify a set of constraints on the sensors’ readings whose satisfaction at time t guarantees collision-freedom during the time interval \([t, t + \varDelta t]\). Here, \(\varDelta t\) is a parameter whose value is bounded by a function of the maximum velocity of the robot and the range of the sensors. The constraints are obtained under assumptions about minimum internal angle and minimum edge length of polyhedral obstacles. We apply these constraints in the switching logic of the Simplex architecture to obtain a controller that ensures collision-freedom. Experiments we have conducted are consistent with these claims. To the best of our knowledge, our study is the first to provide runtime assurance that an autonomous mobile robot with limited sensing can navigate without collisions with only limited information about obstacles.
Dung Phan, Junxing Yang, Denise Ratasich, Radu Grosu, Scott A. Smolka, Scott D. Stoller

From First-order Temporal Logic to Parametric Trace Slicing

Abstract
Parametric runtime verification is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper considers the relationship between two widely-used specification approaches to parametric runtime verification: trace slicing and first-order temporal logic. This work is a first step in understanding this relationship. We introduce a technique of identifying syntactic fragments of temporal logics that admit notions of sliceability. We show how to translate formulas in such fragments into automata with a slicing-based semantics. In exploring this relationship, the paper aims to allow monitoring techniques to be shared between the two approaches and initiate a wider effort to unify specification languages for runtime verification.
Giles Reger, David Rydeheard

R2U2: Monitoring and Diagnosis of Security Threats for Unmanned Aerial Systems

Abstract
We present R2U2, a novel framework for runtime monitoring of security properties and diagnosing of security threats on-board Unmanned Aerial Systems (UAS). R2U2, implemented in FPGA hardware, is a real-time, Realizable, Responsive, Unobtrusive Unit for security threat detection. R2U2 is designed to continuously monitor inputs from the GPS and the ground control station, sensor readings, actuator outputs, and flight software status. By simultaneously monitoring and performing statistical reasoning, attack patterns and post-attack discrepancies in the UAS behavior can be detected. R2U2 uses runtime observer pairs for linear and metric temporal logics for property monitoring and Bayesian networks for diagnosis of security threats. We discuss the design and implementation that now enables R2U2 to handle security threats and present simulation results of several attack scenarios on the NASA DragonEye UAS.
Johann Schumann, Patrick Moosbrugger, Kristin Y. Rozier

A Hybrid Approach to Causality Analysis

Abstract
In component-based safety-critical systems, when a system safety property is violated, it is necessary to analyze which components are the cause. Given a system execution trace that exhibits component faults leading to a property violation, our causality analysis formalizes a notion of counterfactual reasoning (“what would the system behavior be if a component had been correct?”) and algorithmically derives such alternative system behaviors, without re-executing the system itself. In this paper, we show that we can improve precision of the analysis if (1) we can emulate execution of components instead of relying on their contracts, and (2) take into consideration input/output dependencies between components to avoid blaming components for faults induced by other components. We demonstrate the utility of the extended analysis with a case study for a closed-loop patient-controlled analgesia system.
Shaohui Wang, Yoann Geoffroy, Gregor Gössler, Oleg Sokolsky, Insup Lee

Short Papers

Frontmatter

Statistical Model Checking of Distributed Adaptive Real-Time Software

Abstract
The problem of estimating quantitative properties of distributed cyber-physical software that coordinate and adapt to uncertain environments is addressed. A domain-specific language, called dmpl, is developed to both describe such a system and a target property. Statistical model checking (SMC) is used to estimate the probability with which the property holds on the system. A distributed SMC tool is developed and described. Virtual machines are used to implement a realistic execution environment, and to isolate simulations from one another. Experimental results on a coordinated multi-robot example are presented.
David Kyle, Jeffery Hansen, Sagar Chaki

Probabilistic Model Checking at Runtime for the Provisioning of Cloud Resources

Abstract
We elaborate on the ingredients of a model-driven approach for the dynamic provisioning of cloud resources in an autonomic manner. Our solution has been experimentally evaluated using a NoSQL database cluster running on a cloud infrastructure. In contrast to other techniques, which work on a best-effort basis, we can provide probabilistic guarantees for the provision of sufficient resources. Our approach is based on the probabilistic model checking of Markov Decision Processes (MDPs) at runtime. We present: (i) the specification of an appropriate MDP model for the provisioning of cloud resources, (ii) the generation of a parametric model with system-specific parameters, (iii) the dynamic instantiation of MDPs at runtime based on logged and current measurements and (iv) their verification using the PRISM model checker for the provisioning/deprovisioning of cloud resources to meet the set goals (This research has been co-financed by the European Union (European Social Fund - ESF) and Greek national funds through the Operational Program “Education and Lifelong Learning of the National Strategic Reference Framework (NSRF) - Research Funding Program: Thales. Investing in knowledge society through the European Social Fund.”).
Athanasios Naskos, Emmanouela Stachtiari, Panagiotis Katsaros, Anastasios Gounaris

Runtime Verification for Hybrid Analysis Tools

Abstract
In this paper, we present the first steps toward a runtime verification framework for monitoring hybrid and cyber-physical systems (CPS) development tools based on randomized differential testing. The development tools include hybrid systems reachability analysis tools, model-based development environments like Simulink/Stateflow (SLSF), etc. First, hybrid automaton models are randomly generated. Next, these hybrid automaton models are translated to a number of different tools (currently, SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using the HyST source transformation and translation tool. Then, the hybrid automaton models are executed in the different tools and their outputs are parsed. The final step is the differential comparison: the outputs of the different tools are compared. If the results do not agree (in the sense that an analysis or verification result from one tool does not match that of another tool, ignoring timeouts, etc.), a candidate bug is flagged and the model is saved for future analysis by the user. The process then repeats and the monitoring continues until the user terminates the process. We present preliminary results that have been useful in identifying a few bugs in the analysis methods of different development tools, and in an earlier version of HyST.
Luan Viet Nguyen, Christian Schilling, Sergiy Bogomolov, Taylor T. Johnson

Suggesting Edits to Explain Failing Traces

Abstract
Runtime verification involves checking whether an execution trace produced by a running system satisfies a specification. However, a simple ‘yes’ or ‘no’ answer may not be sufficient; often we need to understand why a violation occurs. This paper considers how computing the edit-distance between a trace and a specification can explain violations by suggesting correcting edits to the trace. By including information about the code location producing events in the trace, this method can highlight sources of bugs and suggest potential fixes.
Giles Reger

Tool Papers

Frontmatter

StaRVOOrS: A Tool for Combined Static and Runtime Verification of Java

Abstract
We present the tool StaRVOOrS (Static and Runtime Verification of Object-Oriented Software), which combines static and runtime verification (RV) of Java programs. The tool automates a framework which uses partial results extracted from static verification to optimise the runtime monitoring process. StaRVOOrs combines the deductive theorem prover KeY and the RV tool LARVA, and uses properties written using the ppDATE specification language which combines the control-flow property language DATE used in LARVA with Hoare triples assigned to states. We demonstrate the effectiveness of the tool by applying it to the electronic purse application Mondex.
Jesús Mauricio Chimento, Wolfgang Ahrendt, Gordon J. Pace, Gerardo Schneider

TiPEX: A Tool Chain for Timed Property Enforcement During eXecution

Abstract
The TiPEX tool implements the enforcement monitoring algorithms for timed properties proposed in [1]. Enforcement monitors are generated from timed automata specifying timed properties. Such monitors correct input sequences by adding extra delays between events. Moreover, TiPEX also provides modules to generate timed automata from patterns, compose them, and check the class of properties they belong to in order to optimize the monitors. This paper also presents the performance evaluation of TiPEX within some experimental setup.
Srinivas Pinisetty, Yliès Falcone, Thierry Jéron, Hervé Marchand

Tutorial Papers

Frontmatter

Machine Learning Methods in Statistical Model Checking and System Design - Tutorial

Abstract
Recent research has seen an increasingly fertile convergence of ideas from machine learning and formal modelling. Here we review some recently introduced methodologies for model checking and system design/parameter synthesis for logical properties against stochastic dynamical models. The crucial insight is a regularity result which states that the satisfaction probability of a logical formula is a smooth function of the parameters of a CTMC. This enables us to select an appropriate class of functional priors for Bayesian model checking and system design. We give a tutorial introduction to the statistical concepts, as well as an illustrative case study which demonstrates the usage of a newly-released software tool, U-check, which implements these methodologies.
Luca Bortolussi, Dimitrios Milios, Guido Sanguinetti

RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial

Abstract
RV-Android is a new freely available open source runtime library for monitoring formal safety properties on Android. RV-Android uses the commercial RV-Monitor technology as its core monitoring library generation technology, allowing for the verification of safety properties during execution and operating entirely in userspace with no kernel or operating system modifications required. RV-Android improves on previous Android monitoring work by replacing the JavaMOP framework with RV-Monitor, a more advanced monitoring library generation tool with core algorithmic improvements that greatly improve resource consumption, efficiency, and battery life considerations. We demonstrate the developer usage of RV-Android with the standard Android build process, using instrumentation mechanisms effective on both Android binaries and source code. Our method allows for both property development and advanced application testing through runtime verification. We showcase the user frontend of RV-Monitor, which is available for public demo use and requires no knowledge of RV concepts. We explore the extra expressiveness the MOP paradigm provides over simply writing properties as aspects through two sample security properties, and show an example of a real security violation mitigated by RV-Android on-device. Lastly, we propose RV as an extension to the next-generation Android permissions system debuting in Android M.
Philip Daian, Yliès Falcone, Patrick Meredith, Traian Florin Şerbănuţă, Shin’ichi Shiriashi, Akihito Iwai, Grigore Rosu

LearnLib Tutorial

An Open-Source Java Library for Active Automata Learning
Abstract
Active automata learning is a promising technique to generate formal behavioral models of systems by experimentation. The practical applicability of active learning, however, is often hampered by the impossibility of realizing so-called equivalence queries, which are vital for ensuring progress during learning and finally resulting in correct models. This paper discusses the proposed approach of using monitoring as a means of generating counterexamples, explains in detail why virtually all existing learning algorithms are not suited for this approach, and gives an intuitive account of TTT, an algorithm designed to cope with counterexamples of extreme length. The essential steps and the impact of TTT are illustrated via experimentation with LearnLib, a free, open source Java library for active automata learning.
Malte Isberner, Bernhard Steffen, Falk Howar

Monitoring and Measuring Hybrid Behaviors A Tutorial

A Tutorial
Abstract
Continuous and hybrid behaviors naturally arise from many dynamical systems. In this tutorial, we present state-of-the-art techniques for qualitative and quantitative reasoning about such behaviors. We introduce Signal Temporal Logic and Timed Regular Expressions as specification languages that we use to describe properties of hybrid systems. We then provide an overview of methods for (1) checking whether a hybrid behavior is correct and robust with respect to its specification; and (2) measuring of quantitative characteristics of a hybrid system by property-driven extraction of relevant data from its behaviors. We present the tools that support such analysis and discuss their application in several application domains.
Dejan Ničković

Software Competitions

Frontmatter

Second International Competition on Runtime Verification CRV 2015

CRV 2015
Abstract
We report on the Second International Competition on Runtime Verification (CRV-2015). The competition was held as a satellite event of the 15th International Conference on Runtime Verification (RV’15). The competition consisted of three tracks: offline monitoring, online monitoring of C programs, and online monitoring of Java programs. This report describes the format of the competition, the participating teams and submitted benchmarks. We give an example illustrating the two main inputs expected from the participating teams, namely a benchmark (i.e. a program and a property on this program) and a monitor for this benchmark. We also propose some reflection based on the lessons learned.
Yliès Falcone, Dejan Ničković, Giles Reger, Daniel Thoma

Rigorous Examination of Reactive Systems: The RERS Challenge 2015

The RERS Challenge 2015
Abstract
In this paper we present the RERS challenge 2015, a free-style program analysis challenge on reactive systems to evaluate the effectiveness of different validation and verification techniques. It brings together researchers from different areas including static analysis, model checking, theorem proving, symbolic execution, and testing. The challenge characteristics and set-up are discussed, while special attention is given to the Runtime Verification track that was newly introduced.
Maren Geske, Malte Isberner, Bernhard Steffen

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise