Invited Talks and Tutorials

Compositional Approach to Monitoring Linear Temporal Logic Properties

Amir Pnueli, New York University and Weizmann Institute of Science (Emeritus)

A central component in model checking temporal properties of systems and their run-time monitoring is the translation of a temporal formula, expressing a property of interest, into a corresponding automaton. According to the standard translation, automaton A corresponds to Temporal formula f if the set of sequences accepted by A is precisely the set of sequences that satisfy f. This implies that the correspondence between A and f is required only at the initial position of each sequence.

In this talk we endorse a stronger notion of translation, in which the automaton A_f, called the TEMPORAL TESTER of formula f, has a Boolean output variable x such that x=1 at position j of a sequence s iff (s,j) |= f. Thus, we can view a tester as a TRANSDUCER which, at any position in a behavior, tells us whether the formula f holds at that position. We will describe several advantages of the temporal tester construct. The construction of temporal testers is modular. That is, the temporal tester of a formula "f op g", where "op" can be any Boolean or temporal operator applied to arbitrary temporal formulas f and g, can be constructed by combining the temporal testers of f, g, and "op". As a result, we can outline a model-checking algorithm for LTL formulas which is compositional in the structure of the formula. This type of compositionality has been long considered to be a unique feature of CTL. Based on this approach to LTL model checking, we can obtain a compositional method for model-checking arbitrary CTL* formulas.

We will show how the notion of temporal testers is easily and naturally extended to deal with past formulas and many of the new operators introduced in the Hardware Property Specification language PSL. Another important development, is the use of temporal testers for the modular translation of Metric Interval Temporal Logic (MITL) formulas into Timed Automata.

The results for PSL have been developed jointly with Alex Zaks. The results for MITL have been obtained jointly with Oded Maler and Dejan Nickovic.

Runtime Verification using MOP

Grigore Rosu (UIUC)

This tutorial shows how the Monitoring Oriented Programming (MOP) paradigm can be used to verify programs at runtime. In MOP, runtime monitoring is supported and encouraged as a fundamental principle for building reliable software: monitors are automatically synthesized from specified properties and integrated into the original system to check its dynamic behaviors. When certain conditions of interest occur, such as a violation of a specification, user-defined actions will be triggered, which can be any code from information logging to runtime recovery. Two instances of MOP are discussed: JavaMOP (for Java programs) and BusMOP (for monitoring PCI bus traffic). The architecture of MOP is discussed, and a brief explanation of parametric trace monitoring and its implementation is given. Finally, a comprehensive evaluation of JavaMOP attests to its efficiency, especially with respect to similar systems; BusMOP, in general, imposes 0 runtime overhead on the system it is monitoring.

Verification, Testing and Statistics

Sriram Rajamani (Microsoft Research India)

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:

• We propose using statistical techniques to raise the level of abstraction, and automate the tedium in writing detailed specifications. We present our experience with the MERLIN project where we have used to infer specifications for secure information flow, and discovered several vulnerabilities in web applications
• We propose combining testing with verification to help scalability, an reducing false errors. We present our experience with the YOGI project where we have built a verifier that combines static analysis with testing to find bugs and verify properties of low-level systems code.

Rule-based Systems for Runtime Verification and Log File Analysis

Howard Barringer (Manchester University), Klaus Havelund (JPL, Nasa)

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.

We conclude with a brief description of the current effort to unify these two systems.

Parameterized Unit Testing with Pex, a White Box Test Input Generation Tool for .NET

Nikolai Tillmann, Microsoft Research

This tutorial shows how Parameterized Unit Tests (PUTs), a generalization of traditional unit tests, can be leveraged for systematic testing. PUTs are algebraic specifications written as code, describing the behavior of a program from a client's point of view. Traditional test cases can be obtained by supplying test inputs. Pex is a white box test input generation tool which analyzes the code of PUTs together with the program-under-test to determine relevant test inputs fully automatically. To this end, Pex performs dynamic symbolic execution, where the program is executed multiple times with different inputs while the taken execution paths are monitored. An SMT-solver with model-generation capabilities computes new test inputs that will exercise different execution paths. As a side effect of the analysis, Pex exposes bugs. The result is a traditional unit test suite with high code coverage. Pex has been used in Microsoft to test core .NET components. Pex is integrated in Visual Studio, and publicly available as an MSDN DevLabs project. This tutorial will also give a glimpse of CHESS, a related tool which explores the non-determinism induced by the scheduler, and Code Contracts, a language-agnostic way to express and check preconditions, postconditions and invariants of .NET code.