Parametrized verification of distributed cyber-physical systems: An aircraft landing protocol case study

Taylor T. Johnson, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In this paper, we present the formal modeling and automatic parameterized verification of a distributed air traffic control protocol called the Small Aircraft Transportation System (SATS). Each aircraft is modeled as a timed automaton with (possibly unbounded) counters. SATS is then described as the composition of N such aircraft, where N is a parameter from the natural numbers. We verify several safety properties for arbitrary N, the most important of which is separation assurance, which ensures that no two aircraft may ever collide. The verification methodology relies on computing the set of backward reachable states from the set of unsafe states to a fixed point, and checking emptiness of the intersection of these reachable states and the initial set of states. We used the Model Checker Modulo Theories (MCMT) tool, which implements this technique.

Original languageEnglish (US)
Title of host publicationProceedings - 2012 IEEE/ACM 3rd International Conference on Cyber-Physical Systems, ICCPS 2012
Pages161-170
Number of pages10
DOIs
StatePublished - May 31 2012
Event2012 IEEE/ACM 3rd International Conference on Cyber-Physical Systems, ICCPS 2012 - Beijing, China
Duration: Apr 17 2012Apr 19 2012

Publication series

NameProceedings - 2012 IEEE/ACM 3rd International Conference on Cyber-Physical Systems, ICCPS 2012

Other

Other2012 IEEE/ACM 3rd International Conference on Cyber-Physical Systems, ICCPS 2012
Country/TerritoryChina
CityBeijing
Period4/17/124/19/12

Keywords

  • air traffic control
  • cyber-physical systems
  • hybrid systems
  • verification

ASJC Scopus subject areas

  • Computer Networks and Communications

Fingerprint

Dive into the research topics of 'Parametrized verification of distributed cyber-physical systems: An aircraft landing protocol case study'. Together they form a unique fingerprint.

Cite this