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

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.