Published: 28th March 2010|
|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|
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.
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.
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.
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