Parameterized Verification of Distributed Cyber-Physical Systems: An Aircraft Landing Protocol Case Study

Johnson, Taylor T.; Mitra, Sayan

doi:10.1109/ICCPS.2012.24

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.

Reference:

Taylor T. Johnson, Sayan Mitra, "Parameterized Verification of Distributed Cyber-Physical Systems: An Aircraft Landing Protocol Case Study", In Proceedings of the 3rd ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS 2012), Beijing, China, pp. 161–170, 2012, apr. (source code)

Bibtex Entry:

@inproceedings{johnson2012iccps,
        author          =       {Taylor T. Johnson and Sayan Mitra},
        title           =       {Parameterized Verification of Distributed Cyber-Physical Systems: An Aircraft Landing Protocol Case Study},
        year            =       {2012},
        booktitle       =       {Proceedings of the 3rd ACM/IEEE International Conference on Cyber-Physical Systems (<a href="http://iccps2012.cse.wustl.edu/">ICCPS 2012</a>)},
    address     =   {Beijing, China},
        month           =       apr,
        pages           =       {161--170},
        gsid        =   {11740586308134469378},
        doi     =   {10.1109/ICCPS.2012.24},
        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.},
        comment     =   {<a href="research/iccps2012/">source code</a>},
        pdf = {http://www.taylortjohnson.com/research/johnson2012iccps.pdf},
}