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

Taylor T. Johnson, Sayan Mitra

Research output: Contribution to conferencePaper

Abstract

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.

Original languageEnglish (US)
StatePublished - Sep 16 2013
EventAIAA Infotech at Aerospace (I at A) Conference - Boston, MA, United States
Duration: Aug 19 2013Aug 22 2013

Other

OtherAIAA Infotech at Aerospace (I at A) Conference
CountryUnited States
CityBoston, MA
Period8/19/138/22/13

Fingerprint

Aircraft
Network protocols
Collision avoidance
Landing
Cyber Physical System

ASJC Scopus subject areas

  • Aerospace Engineering

Cite this

Johnson, T. T., & Mitra, S. (2013). Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems. Paper presented at AIAA Infotech at Aerospace (I at A) Conference, Boston, MA, United States.

Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems. / Johnson, Taylor T.; Mitra, Sayan.

2013. Paper presented at AIAA Infotech at Aerospace (I at A) Conference, Boston, MA, United States.

Research output: Contribution to conferencePaper

Johnson, TT & Mitra, S 2013, 'Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems' Paper presented at AIAA Infotech at Aerospace (I at A) Conference, Boston, MA, United States, 8/19/13 - 8/22/13, .
Johnson TT, Mitra S. Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems. 2013. Paper presented at AIAA Infotech at Aerospace (I at A) Conference, Boston, MA, United States.
Johnson, Taylor T. ; Mitra, Sayan. / Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems. Paper presented at AIAA Infotech at Aerospace (I at A) Conference, Boston, MA, United States.
@conference{c4bf7b8fb1114be0b5c9a0a2eab09130,
title = "Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems",
abstract = "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.",
author = "Johnson, {Taylor T.} and Sayan Mitra",
year = "2013",
month = "9",
day = "16",
language = "English (US)",
note = "AIAA Infotech at Aerospace (I at A) Conference ; Conference date: 19-08-2013 Through 22-08-2013",

}

TY - CONF

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

AU - Johnson, Taylor T.

AU - Mitra, Sayan

PY - 2013/9/16

Y1 - 2013/9/16

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84883723847&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84883723847&partnerID=8YFLogxK

M3 - Paper

AN - SCOPUS:84883723847

ER -