Invited talk (Thursday): Klaus Havelund
Jet Propulsion Laboratory, USA
Experiences with Rule-Based Analysis of Spacecraft Logs
Abstract: Runtime verification (RV) consists in part of checking execution traces against user-provided formalized specifications. Throughout the last decade many new systems have emerged, most of which support specification notations based on state machines, regular expressions, temporal logic, or grammars. The field of Artificial Intelligence (AI) has for an even longer period of time studied rule-based production systems, which at a closer look appear to be relevant for RV, although seemingly focused on slightly different application domains, such as for example business processes and expert systems. The core algorithm in many of these systems is the Rete algorithm. We have implemented a rule-based system, named LogFire, for runtime verification, founded on the Rete algorithm, as an internal DSL in the Scala programming language (in essence a library). Using Scala's support for defining DSLs allows us to write rules elegantly as part of Scala programs. This combination appears attractive from a practical point of view. LogFire is currently running daily, analyzing telemetry emitted by the Curiosity rover on Mars. The analysis provides input to a visualization tool, which gives mission operators an overview of the activities on board the rover. We illustrate the effectiveness of combining specification-based log analysis and visualization. We will discuss this application and identify pros and cons of the approach.
Short bio: Dr. Klaus Havelund is a Senior Research Scientist at NASA's Jet propulsion Laboratory (JPL), in the Laboratory for Reliable Software (LaRS). Before joining JPL in 2006, he spent eight years at NASA Ames Research Center in Silicon Valley, California, and one year with Kestrel Technology, a company focusing on commercializing formal methods. He has many years of experience in research and application of formal methods and rigorous software development techniques for critical systems. This includes topics such as programming language semantics, specification language design, theorem proving, model checking, static analysis (developing coding standards), and dynamic analysis. Past work includes participating in the design of the RAISE Specification Language (RSL), a wide-spectrum specification language inspired by VDM, Z and process algebra, and co-writing the associated textbook. He initiated the Java PathFinder project at NASA Ames, a model checker for Java, creating the first prototype of this system, translating Java to the input language of the SPIN model checker. His current main focus of interest is on expressive specification notations for dynamic analysis and their integration with high-level programming languages. He co-started the Runtime Verification (RV) conference. He earned his PhD in Computer Science at the University of Copenhagen, Denmark, which in part was carried out at Ecole Normale Superieure in Paris, France, followed by a post-doc at Ecole Polytechnique and Paris 6, Paris. He spent one year as a research associate at Aalborg University in Denmark.
Invited talk (Friday): Thomas Noll
RWTH Aachen University, Germany
Safety, Dependability and Performance Analysis of Aerospace Systems
Abstract: The size and complexity of software in spacecraft is rapidly increasing, and this trend complicates its design and validation within the context of the overall system. The need for an integrated system-software co-engineering framework is therefore pressing. However, current tools and formalisms tend to be tailored to specific analysis techniques and do not sufficiently cover the full spectrum of required system aspects such as safety, dependability and performability. Moreover, they cannot properly handle the intertwining of hardware and software operation. As such, current engineering practice lacks integration and coherence.
This talk gives an overview of a multidisciplinary and coherent approach to system-software co-engineering of real-time embedded systems. We show how to model such systems and their possible failures using a variant of the Architecture and Analysis Design Language AADL, how to formalize their behavior, and how to analyze them by means of model checking and related techniques.
Short bio: Thomas Noll is an Associate Professor in the Computer Science Department at RWTH Aachen University, Germany. His research area is modeling and verification techniques for software and systems. Current activities concentrate on formal methods for ensuring correctness, performance and dependability of safety-critical systems especially in the aerospace domain, abstraction and verification techniques for pointer programs handling unbounded heap structures, and the verification of programmable logic controller code.