FMA
Formal Methods for Aerospace
The workshop is intended to be a forum for
researchers and practitioners interested in formal techniques for space systems
and air traffic control. These application domains are highly multi and interdisciplinary, and specific formal methods should be
integrated with techniques from control engineering and artificial
intelligence. There will be opportunities to attend lectures given by high
profile experts, presentations of high quality technical contributions, and
discussions sessions.
A major objective
is to promote the holistic view and interdisciplinary methods for design,
verification and co-ordination of aeronautical 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 un-precedent integration of heterogeneous techniques, as well
as deep integration of formal models.
The coexistence of multiple disciplinary perspectives on
the same class of applications (aeronautics) and investigation (formal) methods
leads naturally to the opportunity to define interdisciplinary approaches. The
expected outcomes of this initiative might underline the importance of some
research problems from aeronautics to the formal method community; promote new
formal techniques combining principle of artificial intelligence and control
engineering.
The source of new problems as defined in (A) comes from
the great diversity of aeronautical systems. These can be satellites, UAV
(unmanned aerial vehicles), terrestrial or other kinds of flying robots. These
systems can be involved in complex activities like outer space exploration,
telecommunication support, fire detection, geo-mapping, weather prognoses,
geo-rectification, search & rescue, naval traffic surveillance, tracking
high value targets. From these applications, new research problems and appear:
autonomy, collective behaviour, information fusion, cognitive skills,
coordination, flocking; and new concepts: digital pheromones, swarms, system of
systems of robots, sensing, physical actuation, and so on.
The aeronautical systems are not only safety critical,
but also mission critical and with 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,
aeronautics enrich the traditional formal method topics with new (or, at least,
less investigated) research issues.
Considering the nature of research problems, interdisciplinarity seems to be the natural way to follow.
Formal method approaches could richly benefit from the integration with methods
from other disciplines. Many such opportunities are easily at hand. A good
example is the problem of coordination for platoons of UAV or satellites, which
have been successfully, tackled using various techniques from control
engineering and numerical tools from dynamic programming. As well, there exist
an abundance of examples of using artificial intelligence techniques in
aeronautics (target tracking, rover planning, multi-agent technologies and so
on). The implementation of these methods could benefit from a formal
development. From the cross-fertilization of related multidisciplinary
approaches, we expect more robust, safe and mechanizable
development and verification methods for aeronautical systems.