Runtime Verification

In this tutorial, we introduce two rule-based systems for on and off-line trace analysis, RuleR and LogScope. RuleR is a conditional rule-based system, which has a simple and easily implemented algorithm for effective runtime verification, and into which one can compile a wide range of temporal logics and other specification formalisms used for runtime verification. Specifications can be parameterized with data, or even with specifications, allowing for temporal logic combinators to be defined. We outline a number of simple syntactic extensions of core RuleR that can lead to further conciseness of specification but still enabling easy and efficient implementation. RuleR is implemented in Java and we will demonstrate its ease of use in monitoring Java programs. LogScope is a derivation of RuleR adding a simple very user-friendly temporal logic. It was developed in Python, specifically for supporting testing of spacecraft flight software for NASA’s next 2011 Mars mission MSL (Mars Science Laboratory). The system has been applied by test engineers to analysis of log files generated by running the flight software. Detailed logging is already part of the system design approach, and hence there is no added instrumentation overhead caused by this approach. While post-mortem log analysis prevents the autonomous reaction to problems possible with traditional runtime verification, it provides a powerful tool for test automation. A new system is being developed that integrates features from both RuleR and LogScope.

Though formal verification is the holy grail of software validation, practical applications of verification run into two major challenges. The first challenge is in writing detailed specifications, and the second challenge is in scaling verification algorithms to large software. In this talk, we present possible approaches to address these problems:

A lot of constrained systems still use interpreters to run mobile applications written in Java. These interpreters demand for only a few resources. On the other hand, it is difficult to apply optimizations during the runtime of the application. Annotations could be used to achieve a simpler and faster code analysis, which would allow optimizations even for interpreters on constrained devices. Unfortunately, there is no viable way of transporting annotations to and verifying them at the code consumer. In this paper we present type-separated bytecode as an intermediate representation which allows to safely transport annotations as type-extensions. We have implemented several versions of this system and show that it is possible to obtain a performance comparable to Java Bytecode, even though we use a type-separated system with annotations.

The underlying property, its definition and representation play a major role when monitoring a system. Having a suitable and convenient framework to express properties is thus a concern for runtime analysis. It is desirable to delineate in this framework the spaces of properties for which runtime verification approaches can be applied to.

This paper presents a unified view of runtime verification and enforcement of properties in the safety-progress classification. Firstly, we characterize the set of properties which can be verified (monitorable properties) and enforced (enforceable properties) at runtime. We propose in particular an alternative definition of “property monitoring” to the one classically used in this context. Secondly, for the delineated spaces of properties, we obtain specialized verification and enforcement monitors.

Symbolic execution can be used to explore the possible run-time states of a program. It makes use of a concept of “state” where a variable’s value has been replaced by an expression that gives the value as a function of program input. Additionally, a state can be equipped with a summary of control-flow history: a “path constraint” keeps track of the class of inputs that would have caused the same flow of control. But even simple programs can have trillions of paths, so a path-by-path analysis is impractical. We investigate a “state joining” approach to making symbolic execution more practical and describe the challenges of applying state joining to the analysis of unmodified Linux x86 executables. The results so far are mixed, with good results for some code. On other examples, state joining produces cumbersome constraints that are more expensive to solve than those generated by normal symbolic execution.

This paper describes an interface specification language designed in the LIME project (LIME ISL) and the supporting runtime monitoring tool. The interface specification language is tailored for the Java programming language and supports two kinds of specifications: (i) call specifications that specify requirements for the allowed call sequences to a Java object instance and (ii) return specifications that specify the allowed behaviors of the Java object instance. Both the call and return specifications can be expressed with Java annotations in several different ways: as past time LTL formulas, as (safety) future LTL formulas, as regular expressions, and as nondeterministic finite automata. We also describe the supporting LIME interface monitoring tool which is an open source implementation of runtime monitoring for the interface specifications implemented using AspectJ.

We propose a framework for fault diagnosis that relies on a formal specification that links system behavior and faults. This specification is not intended to model system behavior, but only to capture relationships between properties of system behavior (defined separately) and the faults. In this paper we use a simple specification language: assertions written in propositional logic (possible extensions are also discussed). These assertions can be used together with a combined on-line/off-line diagnostic system to provide a symbolic diagnosis, as a propositional formula that represents which faults are known to be present or absent. Our framework guarantees monotonicity (more knowledge about properties implies more knowledge about faults) and allows to explicitly talk about diagnosability, implicit assumptions on behaviors or faults, and consistency of specifications. State-of-the-art diagnosis frameworks, in particular from the automotive domain, can be cast and generalized in our framework.

Monitoring of software’s execution is crucial in numerous software development tasks. Current monitoring efforts generally require extensive instrumentation of the software or dedicated hardware test rig designed to provide visibility into the software. To fully understand software’s behavior, the production software must be studied in its production environment. To address this fundamental software engineering challenges, we propose a compiler and hardware supported framework for monitoring and observation of software-intensive systems.

We place three fundamental requirements on our monitoring framework. The monitoring must be non-intrusive, low-overhead, and predictable so that the software is not unduly disturbed. The framework must also allow low-level monitoring and be highly flexible so we can accommodate a broad range of crucial monitoring activities.

The general idea behind our work is that to make dramatic progress in non-intrusive, predictable, and fine-grained monitoring, we must change how software is compiled and how hardware is designed; a software-monitoring framework covering the development of monitors, through compilation, and down to the hardware is essential. To achieve our goals, we have pursued an approach leveraging the rapid emergence of multi-core processor architectures to achieve a non-intrusive, predictable, fine-grained, and highly flexible general purpose monitoring framework.

In this report we describe our initial steps in this direction and provide some preliminary performance results achieved with this new multi-core architecture. We use separate cores for the execution of the application to be monitored and the monitors. We augment each core with identical programmable extraction logic that can observe an application executing on the core as its program state changes.

We consider monitoring and checking formally specified properties in a network. We are addressing the problem of deploying the checkers on different network nodes that provide correct and efficient checking. We present the DMaC system that builds upon two bodies of work: the Monitoring and Checking (MaC) framework, which provides means to monitor and check running systems against formally specified requirements, and declarative networking, a declarative domain-specific approach for specifying and implementing distributed network protocols. DMaC uses a declarative networking system for both specifying network protocols and performing checker execution. High-level properties are automatically translated from safety property specifications in the MaC framework into declarative networking queries and integrated into the rest of the network for monitoring the safety properties. We evaluate the flexibility and efficiency of DMaC using simple but realistic network protocols and their properties.