RV-CuBES 2017: Papers with Abstracts

Abstract. RV-CuBES was an international workshop that took place alongside the 17th International Conference on Runtime Verification in Seattle during 13-16th September, 2017. The focus of the competition was to consider tools for Runtime Verification (RV). The acronym CuBES stands for Competitions, usability, Benchmarks, Evaluation, and Standardisation. The workshop consisted of poster presentations of tool overview papers and a discussion session of position papers. This report gives an overview of submissions and discussions.

Abstract. In this paper we give an overview of Valour, a runtime verification tool which has been developed in the context of a project to act as a backend verification tool for financial transaction software. A Valour script is written by the user and is then compiled into a verification system. Although, developed as part of a project, the tool has been designed as a stand-alone general-purpose verification engine with a particular emphasis on event consumption. The strong points of Valour when compared to other runtime verification tools is its focus on scalability and robustness.

Abstract. MonPoly is a monitoring tool for checking logs against formulas of metric first-order temporal logic. We provide here an overview of the tool, including its usage and history.

Abstract. We present Aerial, a tool for the online monitoring of metric regular properties. Aerial supports both the standard metric temporal logic (MTL) and the more expressive meric dynamic logic (MDL) as its property specification language. Unlike MTL, which is restricted to star-free properties, MDL can express all metric regular properties by generalizing MTL’s temporal operators to arbitrary regular expressions. Aerial’s distinguishing feature is its ability to monitor an event stream using memory logarithmic in the event rate. This space efficiency is achieved by altering how Aerial outputs its monitoring verdicts.

Abstract. In this position paper we discuss the risk of tool over-tuning in
runtime verification competitions. We believe that the risk is
inherently enabled by the format of the competitions and we discuss it
in the context of the "First International Competition on Software
for Runtime Verification (CSRV~2014)", in which we participated.

Abstract. Ensuring formal correctness for actor-based, concurrent systems is a difficult task, pri- marily because exhaustive, static analysis verification techniques such as model checking quickly run into state-explosion problems. Runtime monitoring techniques such as Run- time Verification and Adaptation circumvent this limitation by verifying the correctness of a program by dynamically analysing its executions. This paper gives an overview of a suite of monitoring tools available for verifying and adapting actor-based Erlang programs.

Abstract. Aspect oriented programming (AOP) is an instrumentation mechanism that is generally employed by runtime monitoring frameworks to automatically extract system events and embed monitoring code within an existing system. Although several AOP tools exist for renowned languages such as Java and C#, little to no tools have been developed for actor oriented languages such as Erlang. We present eAOP, an AOP tool specifically designed to instrument actor-oriented constructs in Erlang such as message sends and receives, along with other traditional constructs such as function calls.

Abstract. Larva, which has been in use and continuous development for almost a decade, has been extended in several ways and used in a wide range of scenarios, from industrial deployment to educational ones. In this paper we give an overview of Larva and give an overview of its extensions and uses.

Abstract. TemPsy (Temporal Properties made easy) is a pattern-based, domain-specific language for the specification of temporal properties. In this paper we provide an overview of TemPsy-Check, a tool that implements a model-driven approach for performing offline trace checking of temporal properties written in TemPsy. TemPsy-Check relies on an optimized mapping of temporal requirements written in TemPsy into Object Constraint Language (OCL) constraints on a conceptual model of execution traces.

Abstract. We introduce the DANA platform for specifying and analyzing networked applications. DANA was originally created targeting the automotive domain for the verification and validation of software interface behavior in new infotainment and advanced driver assistant systems that are integrated on a single hardware platform. The messages in these interfaces can contain complex data, e.g., playlists with images. Therefore, valid behavior is described as a layered reference model. The platform can use the model to generate test cases, code for simulation, and to verify a live or recorded trace. Exchangeable resumption algorithms enable DANA to resume runtime verification after a deviation using the original state machine without manual changes. A generic input model allows quick integration of new sources for messages. Therefore, DANA can easily be applied to other domains where interactive behavior can be observed. In this paper, we present the tool, its layered reference model, and show its application for runtime verification.

Abstract. This paper is a short introduction to the BeepBeep 3 event stream processor. It highlights the main design decisions that informed its development, and the features that distinguish it from other Runtime Verification tools.

Abstract. Over the past five years, we have met with representatives of more than a dozen companies in various domains, trying to showcase the features of our runtime verification tool. These meetings gave us some very instructive feedback about the way RV is perceived by people from the industry, and about the shortcomings of current RV solutions. In this paper, we discuss a few of the comments we heard, and use them to suggest new ways of developing and evaluating RV tools in the future.

Abstract. The runtime verification community is still fragmented with non-interoperable specifications and tools. Within the EU H2020 project COEMS “Continuous Observation of Embedded Multicore Systems”, we are contributing to the European Open Research Data Pilot that makes scientific data available to other researchers. We describe our first contributions and experience with the required data management and discuss technical issues such as metadata management, format and storage on practical examples. Based on our experience, we make suggestions on tools and formats for future RV Competitions and for desired artefacts from the EU COST Action IC1402 "ARVI -- Runtime Verification Beyond Monitoring".

Abstract. This work is related to our monitoring tool called ARTiMon for the online property monitoring of discrete and continuous systems. This paper presents the syntax and the semantics of the current input language of ARTiMon. Because this is not always well understood by users, and also because it grounds the ability of ARTiMon to check properties online, in this tool paper a particular focus is accorded to the domain definition of time functions used to interpret terms of the language.

Abstract. The need for runtime verification (RV), and tools that enable RV in practice, is widely recognized. Systems that need to operate autonomously necessitate on-board RV technolo- gies, from Mars rovers that need to sustain operation despite delayed communication from operators on Earth, to Unmanned Aerial Systems (UAS) that must fly without a human on-board, to robots operating in dynamic or hazardous environments that must take care to preserve both themselves and their surroundings. Enabling all forms of autonomy, from tele-operation to automated control to decision-making to learning, requires some ability for the autonomous system to reason about itself. The broader class of safety-critical systems require means of runtime self-checking to ensure their critical functions have not degraded during use.
Runtime verification addresses a vital need for self-referential reasoning and system health management, but there is not currently a generalized approach that answers the lower-level questions. What are the inputs to RV? What are the outputs? What level(s) of the system do we need RV tools to verify, from bits and sensor signals to high-level architectures, and at what temporal frequency? How do we know our runtime verdicts are correct? How do the answers to these questions change for software, hardware, or cyber-physical systems (CPS)? How do we benchmark RV tools to assess their (comparative) suitability for particular platforms? The goal of this position paper is to fuel the discussion of ways to improve how we evaluate and compare tools for runtime verification, particularly for cyber-physical systems.

Abstract. R2U2 (Realizable, Responsive, Unobtrusive Unit) is an extensible framework for runtime System Health Management (SHM) of cyber-physical systems. R2U2 can be run in hardware (e.g., FPGAs), or software; can monitor hardware, software, or a combination of the two; and can analyze a range of different types of system requirements during runtime. An R2U2 requirement is specified utilizing a hierarchical combination of building blocks: temporal formula runtime observers (in LTL or MTL), Bayesian networks, sensor filters, and Boolean testers. Importantly, the framework is extensible; it is designed to enable definitions of new building blocks in combination with the core structure. Originally deployed on Unmanned Aerial Systems (UAS), R2U2 is designed to run on a wide range of embedded platforms, from autonomous systems like rovers, satellites, and robots, to human-assistive ground systems and cockpits.
R2U2 is named after the requirements it satisfies; while the exact requirements vary by platform and mission, the ability to formally reason about Realizability, Responsiveness, and Unobtrusiveness is necessary for flight certifiability, safety-critical system assurance, and achievement of technology readiness levels for target systems. Realizability ensures that R2U2 is sufficiently expressive to encapsulate meaningful runtime requirements while maintaining adaptability to run on different platforms, transition be- tween different mission stages, and update quickly between missions. Responsiveness entails continuously monitoring the system under test, real-time reasoning, reporting intermediate status, and as-early-as-possible requirements evaluations. Unobtrusiveness ensures compliance with the crucial properties of the target architecture: functionality, certifiability, timing, tolerances, cost, or other constraints.

Abstract. This short paper presents a compilation of feedback about online runtime verification competitions from an active contestant. In particular, it points out several issues and how they could possibly be fixed.

Abstract. This tool paper presents E-ACSL, a runtime verification tool for C programs capable of checking a broad range of safety and security properties expressed using a formal specification language. E-ACSL consumes a C program annotated with formal specifications and generates a new C program that behaves similarly to the original if the formal properties are satisfied, or aborts its execution whenever a property does not hold. This paper presents an overview of E-ACSL and its specification language.