Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems

In this paper, we describe a method for synthesizing inductive invariants for cyber-physical aerospace systems that are parameterized on the number of participants, such as the number of aircraft involved in a coordinated maneuver. The methodology is useful for automating the traditionally manual process of deductive verification of safety properties, such as collision avoidance, and establishes such properties regardless of the number of participants involved in a protocol. We illustrate the methodology using a simplified model of the landing protocol of the Small Aircraft Transportation System (SATS) as a case study. Each participant (aircraft) in the protocol is modeled as a hybrid automaton with both discrete and continuous states and potentially nondeterministic evolution thereof. Discrete states change instantaneously according to transitions and continuous states evolve according to rectangular differential inclusions. The invariant synthesis method enables a fully automatic verification of the main safety property of SATS, namely, safe separation of aircraft on approach to the runway. The method is implemented in a prototype verification tool called Passel. We present promising experimental results using the methodology, which has enabled a fully automatic proof of safe separation for the model of SATS.