Published: 28th March 2010
DOI: 10.4204/EPTCS.20
ISSN: 2075-2180

EPTCS 20

Proceedings FM-09 Workshop on
Formal Methods for Aerospace
Eindhoven, The Netherlands, 3rd November 2009

Edited by: Manuela Bujorianu and Michael Fisher

Preface
Manuela Bujorianu and Michael Fisher
Bisimulation Relations Between Automata, Stochastic Differential Equations and Petri Nets
Mariken H.C. Everdij and Henk A.P. Blom
1
An Entry Point for Formal Methods: Specification and Analysis of Event Logs
Howard Barringer, Alex Groce, Klaus Havelund and Margaret Smith
16
Modelling and Verification of Multiple UAV Mission Using SMV
Gopinadh Sirigineedi, Antonios Tsourdos, Rafał \.Zbikowski and Brian A. White
22
Implementing Multi-Periodic Critical Systems: from Design to Code Generation
Julien Forget, Frédéric Boniol, David Lesens and Claire Pagetti
34
Re-verification of a Lip Synchronization Protocol using Robust Reachability
Piotr Kordy, Rom Langerak and Jan Willem Polderman
49
Agent Based Approaches to Engineering Autonomous Space Software
Louise A. Dennis, Michael Fisher, Nicholas Lincoln, Alexei Lisitsa and Sandor M. Veres
63
Formalization and Validation of Safety-Critical Requirements
Alessandro Cimatti, Marco Roveri, Angelo Susi and Stefano Tonetta
68
Flexible Lyapunov Functions and Applications to Fast Mechatronic Systems
Mircea Lazar
76
Polychronous Interpretation of Synoptic, a Domain Specific Modeling Language for Embedded Flight-Software
Loïc Besnard, Thierry Gautier, Julien Ouy, Jean-Pierre Talpin, Jean-Paul Bodeveix, Alexandre Cortier, Marc Pantel, Martin Strecker, Gérald Garcia, Ana-Elena Rugina, Jérémy Buisson and Fabien Dagnat
80
Developing Experimental Models for NASA Missions with ASSL
Emil Vassev and Mike Hinchey
88

Preface

These electronic proceedings are derived from the workshop on Formal Methods for Aerospace which took place on 3rd November 2009 in Eindhoven, the Netherlands, as an affiliated event of the Formal Methods Week FM2009.

Background

The coexistence of multiple disciplinary perspectives on the same class of critical applications (aerospace) and investigation (formal) methods leads naturally to the opportunity to define multidisciplinary approaches. Thus, work in this area will likely underline the importance of some research problems from aerospace to the formal methods community, and promote new formal techniques combining the principles of artificial intelligence and control engineering.

The source of new problems for formal methods comes from the great diversity of aerospace systems. These can be satellites, unmanned aerial vehicles (UAVs), terrestrial or other kinds of flying robots. These systems can be involved in complex activities such as space exploration, telecommunication support, fire detection, geo-mapping, weather prognoses, geo-rectification, search and rescue, naval traffic surveillance, tracking high value targets. From these applications, new research problems appear: autonomy, collective behaviour, information fusion, cognitive skills, coordination, flocking, etc. In addition, new concepts must be formalised: digital pheromones, swarms, system of systems of robots, sensing, physical actuation, and so on.

Aerospace systems are not only safety critical, but also mission critical and have very high performance requirements. For example, there is no safety issue regarding a planetary rover, but the system performance must justify the great cost of deploying it. Consequently, aerospace enriches traditional formal methods topics with new (or, at least, rarely investigated) research issues.

Formal methods can greatly benefit from integration with approaches from other disciplines, and many such opportunities are now appearing. A good example is the problem of coordination for platoons of UAVs or satellites, which have been successfully, tackled using various techniques from control engineering and numerical tools from dynamic programming. In addition, there exists an abundance of examples of artificial intelligence techniques in aerospace (target tracking, rover planning, multi-agent technologies and so on). The implementation of these methods could benefit from formal development. From the cross-fertilization of related multidisciplinary approaches, we expect more robust, safe and mechanizable development and verification methods for aerospace systems.

Workshop

The main workshop objective was to promote a holistic view and interdisciplinary methods for design, verification and co-ordination of aerospace systems, by combining formal methods with techniques from control engineering and artificial intelligence. The very demanding safety, robustness and performance requirements of these systems require unprecedented integration of heterogeneous techniques and models. The aim of FMA was to bring together active researchers from all the above areas to discuss and present their work. Relevant topics within FMA, specifically with a focus on potential applications in aerospace design or engineering, are:

Format

The workshop comprised three types of activities:
  1. Plenary lectures;
  2. Presentations of peer reviewed contributed papers;
  3. Contributed talks on ongoing research project or recent research trends that are not sufficiently disseminated across relevant academic communities.
Our plenary speakers are well known experts in the area of verification of space systems and area traffic management systems.

Klaus Havelund from the Jet Propulsion Laboratory at NASA introduced the participants to the subtleties of run time verification of the log files for NASA's next 2011 Mars mission MSL (Mars Science Laboratory). The specific challenges include the design of: a suitable specification language; verification algorithms of execution traces against formal specifications; and techniques of combining run time analysis with formal testing.

Henk Blom from the National Laboratory of Aerospace, Amsterdam, introduced the audience into the world of verification for future air traffic management systems from a control engineering perspective. The techniques involved are of probabilistic nature and, in their most general form, are known as stochastic reachability analysis. Although the formal aspects of control engineering verification are less transparent, stochastic reachability analysis is the continuous counterpart of probabilistic model checking, which is a well established formal verification technique.

The contributed talks united experts who very rarely attend a common scientific event. A major objective of the FMA workshop was the cross-fertilization of the multi-disciplinary approaches to the development and verification of aerospace systems. Experts in the area of hybrid systems interacted with experts in software engineering in a quest for improved inter-disciplinary techniques for enhancing the quality of control software in avionics. In addition to formal verification, other topics specific to formal methods were discussed, including observability, multi-agent systems, requirements analysis, synchronous languages, etc.

Steering Committee

Programme Committee

Thanks

We wish to thank the members of the Programme Committee for their careful evaluation of the submitted papers. We would also like to thank all participants for engaging in such a constructive discussion and making the workshop so successful.

We would like to thank the editorial board of the Electronic Proceedings in Theoretical Computer Science (EPTCS) for accepting to publish these contributions in their series.

Finally, we would like to thank the FM Week organisers and administrators for hosting the FMA workshop so capably.

Manuela Bujorianu and Michael Fisher