FMA@CDC

2^nd edition of Formal Methods for Aerospace

Abstracts

In the presentation order

Henk Blom

Stochastic Hybrid Systems Modelling, Bisimulation and Safety Verification of Airborne Self Separation

In spite of advances in formal and probabilistic verification approaches, fault and event trees still are the dominant techniques used for safety risk analysis in aviation. However, the combination of concurrent, dynamic and random effects that appear in air traffic cannot properly be captured by these classical techniques. In this lecture it will be explained how safety risk modeling and analysis can be formulated as a problem of estimating rare event probabilities for a large scale stochastic hybrid system. Subsequently it is explained how rare event estimation theory for diffusions can be extended to a large scale stochastic hybrid system (SHS) where a very huge number of rare discrete modes may contribute significantly to the rare event estimation. Essentially, the approach taken is to develop a compositional model of the air traffic operation considered in the form of a large scale SHS, subsequently to introduce a suitable aggregation of the discrete modes of this large scale SHS, and then to develop importance sampling and Rao-Blackwellization relative to these aggregations. The practical use of this approach is demonstrated for the estimation of mid-air collision probability when aircraft are flying under an airborne self separation concept of operation.

Serdac Karaman

Anytime algorithms for differential games: applications to aerospace systems

Manuela Bujorianu

Logics for Stochastic Hybrid Control Systems

In this talk, we address the issue of logical characterization of reachability analysis of time systems with stochastic features. This problem is now well understood and successfully investigated for probabilistic systems with discrete state change like Markov chains and labelled Markov processes. In the last decade, this problem has been formulated for systems with continuous state change (continuous-time, continuous state). Despite of many investigations in various engineering fields, the techniques from the discrete case could not be extended to the continuous case. In this work, we present a new model theoretic logic that characterizes a bisimulation relation for continuous time continuous space Markov processes. For this logic we define a new semantics using state space symmetries. These are a recent concept that was successfully used in model checking. Using this semantics, we prove a full abstraction result. Moreover, we prove a result that can be used in model checking, namely that the bisimulation preserves the probabilities of the reachable sets.

Antonios Tsourdos

Towards Guaranteed Performance of Dynamic Behaviour of Multiple Unmanned Aerial Vehicles

To ensure guaranteed performance of cooperating UAVs the behaviours of the UAVs have to be modelled for the purpose of analysis and verification of desirable properties. Formal modelling techniques originally evolved around the study of reactive systems. A reactive system is a system which maintains constant interaction with the environment in which it operates. Therefore, its specification must be done in terms of ongoing behaviour over time. This talk presents a formal modelling and verification for a multiple UAV system on surveillance and recognisance mission. Kripke modelling formalism is used to formally model the decentralized cooperative control strategy and the desired system properties are expressed in temporal logic statements. The Kripke model is then subjected to an algorithmic verification technique known as model checking and the validity of the temporal formulae on the model is verified.

Sayan Mitra

Hybrid Modelling and Verification of Aerospace Systems

Hybrid automaton-based modeling and verification of realistic systems has faced several roadblocks both in theoretical scalability of algorithms and in the availability of practical software tools. In this talk, I will describe several ongoing projects at the University of Illinois which attempt to address these issues. First, I will describe the algorithm behind and the implementation of a recent toll (HARE) for counter-example guided abstraction and refinement of hybrid systems, and share our experiences with it. Second, I will discuss a second tool that aims to improve usability of hybrid technologies by building a bridge between the popular Simulink/Stateflow modeling environment and hybrid automata. Finally, I’ll discuss the application of these tools and algorithms in analyzing aerospace applications such as distributed air-traffic control protocols and (possibly) goal networks for aerial robots.

Alessandro Pinto

Stochastic model-based design of Aerospace Systems

The thermal management system of a prototypical aircraft is abstracted and modeled as a stochastic hybrid system. This application is used as the driver to develop computational methods for probabilistic reachability analysis of this class of models. We discuss the challenges faced in the development of these methods and present a tool under development at the United Technologies Research Center.
To overcome the complexity of the analysis problem, we show a practical implementation of contract-based design for this class of systems. The design methodology we developed allows us to analyze the system in its full complexity including thermal management system, control and embedded architecture.

Maria Prandini

Reachability Analysis for Probabilistic Hybrid Systems with Application to Air Traffic Management

A reachability problem consists of determining if the trajectories of some system will eventually enter a pre-specified set. An important application of reachability analysis is the verification of the correct behavior of a system, which makes reachability analysis relevant in a variety of contexts and, in particular, in those safety-critical applications where a certain region of the state space is “unsafe” and one has to verify that the system state keeps outside this unsafe set. In this talk, we describe a methodology for safety analysis of a certain class of probabilistic hybrid systems, and show how it can be useful within the air traffic management context.

Jianghai Hu

Generating functions of randomly switching systems

In this talk, the notion of generating functions is introduced as a framework to study quantitatively the stability and stabilizability of switched systems, including randomly switching systems. Several important quantities, such as the joint spectral radius, Lyapunov exponent, L2-induced gain, stabilizability index, can be characterized uniformly in such a framework. Efficient numerical algorithms will be proposed for the estimations of these quantities. As an example, the application to the consensus problem on randomly changing networks will be discussed.

Kostas Margellos & John Lygeros

4D trajectory management: Reachability theory formulation and target window implementation

4D trajectory management is widely regarded as the basis for the next generation air traffic management systems envisioned by SESAR and NextGen. We discuss how timing requirements inherent in 4D trajectory management can be formulated in the context of reachability theory. We outline methods and computational tools from reachability theory and highlight how they can be adapted to characterize the maneuvering freedom afforded by timing requirements. We also demonstrate how reachability tools can be used to perform conflict resolution while respecting 4D trajectory constraints whenever possible. The discussion is framed in the context of the so-called target windows, a framework that can serve a possible implementation of 4D trajectory management currently under investigation by the CATS project.

Joost-Pieter Katoen

Correctness, Safety and Performance of Aerospace Systems

This talk presents a component-based modelling approach to system-software co-engineering of real-time embedded systems, in particular aerospace systems. Our method is centered around the standardized Architecture Analysis and Design Language (AADL) modelling framework. We formalize a significant subset of AADL, incorporating its recent Error Model Annex for modelling faults and repairs. The major distinguishing aspects of this component-based approach are the possibility to describe nominal hardware and software operations, hybrid (and timing) aspects, as well as probabilistic faults and their propagation and recovery. Moreover, it supports dynamic reconfiguration of components and intercomponent connections. The operational semantics gives a precise interpretation of specifications by providing a mapping onto networks of event-data automata. These networks are then subject to different kinds of formal analysis such as model checking, safety and dependability analysis and performability (i.e., performance under degraded modes of operation) evaluation. We demonstrate tool support realizing these analyses and report on industrial case studies that have been carried out in the context of aerospace systems.