COMPASS 2009 Workshop

Affiliated to the The European Joint Conferences on Theory and Practice of Software (ETAPS 2009), March 29, 2009, York, UK

Aerospace systems such as Spacecraft, Unmanned Aerial Vehicles (UAVs), Air Traffic Control are critical systems for which errors in either software or hardware can be catastrophic. Correctness notions are in fact mostly tightly connected to performance issues. What is the probability of a space mission success? Safety and dependability analysis in nominal as well as in the degraded modes of operation are prominent examples thereof. This calls for combining correctness, safety, dependability, and performance aspects in an integrated approach. This workshop aims to bring together researchers and practitioners that apply or develop (semi-)formal techniques for the modeling, verification, performance, and safety analysis of aerospace (or any critical) systems, aiming to provide a state-of-the-art overview of activities and challenges in the field. Approaches that attempt to combine some of these different aspects are of particular interest.

Areas of interests

Areas of interest for the COMPASS workshop include, but are not limited to:

Program

09:00 Opening

09:15 - 09:45 Overview of the ESA COMPASS Project (Joost-Pieter Katoen, RWTH Aachen University, D)

09:45 - 10:30 Monitoring the Execution of Spacecraft Flight Software (Klaus Havelund, JPL LARS and Caltech, USA)

10:30 - 11:00 Coffee break

11:00 - 11:45 Verification of Synchronous/Asynchronous Systems by Combining Model-Driven Engineering and Formal Methods (Hubert Garavel, INRIA Grenoble Rhone-Alps, F)

11:45 - 12:30 A System-Level Integrated Modeling Language for Aerospace Applications (Thomas Noll, RWTH Aachen University, D)

12:30 - 14:00 Lunch break

14:00 - 14:45 RAMS Software Techniques in European Space Projects, an Industrial View (Juan M. Carranza, European Space Agency, NL)

14:45 - 15:30 Formal Model-Based Development in Aerospace Systems: Challenges to Adoption (Mats Heimdahl, Univ. of Minnesota, USA)

15:30 - 16:00 Tea break

16:00 - 16:45 Symbolic Verification of System-Level Specifications for Aerospace Applications (Marco Roveri, Fondazione Bruno Kessler, I)

16:45 Closing

List of talks

The workshop program includes the following talks.

Overview of the ESA COMPASS Project
Joost-Pieter Katoen (RWTH Aachen University, D)

ABSTRACT: This talk provides an overview of the COMPASS (COrrectness, Modeling, and Performance of Aerospace Systems) project which is funded by the European Space Agency. This project aims to develop a model-based approach to system-software co-engineering which is tailored to the specific characteristics of critical on-board systems for the aerospace domain. We will provide some insight in the modeling language which is based on AADL and its accompanying error annex. It allows for describing nominal hardware and software operation, (probabilistic) faults and their propagation, error recovery, and degraded modes of operation. The modeling is complemented by powerful analysis techniques for correctness, performance, and safety properties. These techniques are based on probabilistic and symbolic model checking.

Monitoring the Execution of Spacecraft Flight Software
Klaus Havelund (JPL LARS and Caltech, USA)

ABSTRACT: The amount of software on spacecraft grows for each new mission. The Mars Exploration Rovers (MER) contained 550,000 lines of code, whereas the next Mars Science Laboratory (MSL) rover will contain close to 3 million lines of code. The number of errors introduced during programming such systems consequently also grows. Unfortunately, due to the tight integration of software and hardware, it is difficult to apply automated test case generation. Just running the software with hardware simulators, or even worse: on real hardware, becomes a bottleneck. A low impact, but effective, methodology is to at least evaluate performed executions properly against expected requirements. The MSL software team employs a programming methodology that includes the insertion of logging statements as part of the code. As a result each system execution produces log files. We have developed a state of the art monitoring technique to evaluate such log files against formal specifications. We shall present this work, with specific emphasis on the development of a rule-based specification language for event sequence monitoring. We shall present the general Java framework RuleR as well as the specialized Python instantiation LogScope, developed for testing MSL. This work has been done in collaboration with: Howard Barringer (U. of Manchester), Alex Groce (JPL), and Margaret Smith (JPL).

Verification of Synchronous/Asynchronous Systems by Combining Model-Driven Engineering and Formal Methods
Hubert Garavel (INRIA Grenoble Rhone-Alpes, F)

ABSTRACT: This talk addresses two challenging issues: (1) How to combine model-driven engineering with formal methods --- this requires to fill many gaps, e.g. between graphical and textual modeling languages, between special-purpose ("domain specific") and general-purpose modelling languages, etc., and (2) How to analyze automatically complex systems consisting of sequential blocks running concurrently and connected via slow or unreliable channels (such as communication protocols or Globally Asynchronous Locally Synchronous hardware circuits). We propose a working approach that is based on the Eclipse/TOPCASED workbench for model-driven engineering and the CADP model checking toolbox for concurrent systems. We illustrate our approach with an industrial case-study provided by Airbus: the verification and performance evaluation for a TFTP/UDP communication link between a plane and the ground.

A System-Level Integrated Modeling Language for Aerospace Applications
Thomas Noll (RWTH Aachen University, D)

ABSTRACT: We give an overview of the System-Level Integrated Modeling (SLIM) Language that has been designed within the COMPASS project, a model-based approach to system-software co-engineering which is tailored to the specific characteristics of critical on-board systems for the aerospace domain. This component-based language provides engineers with convenient ways to describe nominal hardware and software operation, (probabilistic) faults and their propagation, error recovery, and degraded modes of operation. A SLIM specification is hierarchically organized into components which interact through connections via ports allowing for both message and continuous communication, and which can be reconfigured dynamically. Besides showing example applications, we also sketch the formal semantics of the SLIM language, which is defined in terms of dynamic networks of communicating automata.

RAMS Software Techniques in European Space Projects, an Industrial View
Juan M. Carranza (European Space Agency, NL)

ABSTRACT: One of the main functions of ESA is to promote and manage space programmes implemented by industry. This management includes technical monitoring of programmes in many technical disciplines, including software Reliability, Availability, Maintainability and Safety (RAMS) of space systems. This presentation provides an overview of the experience accumulated by the author in monitoring software product assurance activities in space projects over a period of 9 years. This includes a presentation of the RAMS techniques used most frequently by industry to predict the RAMS properties of a space system and the design, implementation and verification of measures to handle failures. The presentation also identifies the main issues found in the implementation of those techniques. The issues found in industrial projects are not only technical but can also be organisational, contractual and even political. The presentation will describe and analyse those issues based on the author's perception. The presentation will also provide a brief overview of some of the R&D activities carried out in the area of software product assurance in relation to software RAMS in as much as they are intended to help industry in implementing RAMS techniques.

Formal Model-Based Development in Aerospace Systems: Challenges to Adoption
Mats Heimdahl (Univ. of Minnesota, USA)

ABSTRACT: There is a movement towards more model-based software development; a shift in development paradigm where the development process is centered on a (formal) model of the intended software behavior, and development is largely driven by tools and automation. This approach to software development holds great promise in that it may be able to help us dramatically increase software quality, reduce cycle time, and reduce development costs. Although there are many success stories reported in the literature, the challenges with adopting model-based techniques are rarely discussed. In our collaborations with industry over the last decade, we have observed many ways in which adoption of these promising techniques can go wrong. In the best case, it is a learning experience for the company involved; in the worst case, the techniques get such a bad reputation they will not be attempted again until there is a change in management. In this talk we will explore these challenges and provide recommendation as to how we --as a community-- may be able to address them and allow industry to reap the full benefits of model-based development.

Symbolic Verification of System-Level Specifications for Aerospace Applications
Marco Roveri (Fondazione Bruno Kessler, I)

ABSTRACT: In this talk we overview the set of functionalities for the verification of the the System-Level Integrated Modeling (SLIM) models, that is being developed within the COMPASS project, a model-based approach to system-software co-engineering. The framework allows for requirements validation, formal property verification, and various forms of dependability analyses, for complex systems with continuous dynamics. The talk will overview the integration of different verification techniques, including symbolic model checking and Satisfiability Modulo Theory, and counter-example guided abstraction refinement.

Organising committee

Alessandro Cimatti
Fondazione Bruno Kessler, Trento, Italy

Joost-Pieter Katoen
RWTH Aachen University, Germany

Yuri A. Yushtein
European Space Agency / ESTEC, Noordwijk, The Netherlands