FTSCS 2014
Third International Workshop on Formal Techniques for Safety-Critical Systems

(An ICFEM 2014 Satellite Event)

Luxembourg, November 6 and 7, 2014


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.

Invited talk: Ian Hayes

School of ITEE, The University of Queensland, Brisbane, Australia

Towards structuring system specifications with time bands using layers of rely-guarantee conditions

The overall specification of a cyber-physical system can be given in terms of the desired behaviour of its physical components operating within the real world. The specification of its control software can then be derived from the overall specification and the properties of the real-world phenomena, including their relationship to the computer system's sensors and actuators. The control software specification them becomes a combination of the guarantee it makes about the system behaviour and the real-world assumptions it relies upon.

Such specifications can easily become complicated because the complete system description deals with properties of phenomena at widely different time granularities, as well as handling faults. To help manage this complexity, we consider layering the specification within multiple time bands, with the specification of each time band consisting of both the rely and guarantee conditions for that band, both given in terms of the phenomena of that band. The overall specification is then the combination of the multiple rely-guarantee pairs. Multiple rely-guarantee pairs can also be used to handle faults.

Bio

Ian Hayes is a Professor in the School of Information Technology and Electrical Engineering at the University of Queensland, Australia. His research interests focus on methods for specifying and reasoning about software and systems. Recent research includes methods for reasoning about concurrent programs in a rely-guarantee style that emphasises the algebraic properties of parallelism and guarantee and rely constructs. A long-term theme of his research has looked at real-time systems. Recently this has examined structuring system specifications using time bands, while earlier research focussed on refinement of real-time systems. His earlier research while at Oxford University focussed on software specification using Abrial's Z specification language.