Scipediacontent: Scipediacontent moved page Draft Content 625578912 to Johnson Mitra 2012a

2021-02-03T15:05:52Z

Scipediacontent moved page Draft Content 625578912 to Johnson Mitra 2012a

Scipediacontent: Created page with " == Abstract == In this paper, we present the formal modeling and automatic parameterized verification of a distributed air traffic control protocol called the Small Aircraft..."

2021-02-03T15:05:49Z

Created page with " == Abstract == In this paper, we present the formal modeling and automatic parameterized verification of a distributed air traffic control protocol called the Small Aircraft..."

New page

== 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 document ==

The different versions of the original document can be found in:

* [http://dx.doi.org/10.1109/iccps.2012.24 http://dx.doi.org/10.1109/iccps.2012.24]

* [http://www.taylortjohnson.com/research/johnson2012iccps.pdf http://www.taylortjohnson.com/research/johnson2012iccps.pdf]

* [http://xplorestaging.ieee.org/ielx5/6197284/6197382/06197398.pdf?arnumber=6197398 http://xplorestaging.ieee.org/ielx5/6197284/6197382/06197398.pdf?arnumber=6197398],
: [http://dx.doi.org/10.1109/iccps.2012.24 http://dx.doi.org/10.1109/iccps.2012.24]

* [https://dblp.uni-trier.de/db/conf/iccps/iccps2012.html#JohnsonM12 https://dblp.uni-trier.de/db/conf/iccps/iccps2012.html#JohnsonM12],
: [http://yadda.icm.edu.pl/yadda/element/bwmeta1.element.ieee-000006197398 http://yadda.icm.edu.pl/yadda/element/bwmeta1.element.ieee-000006197398],
: [https://experts.illinois.edu/en/publications/parametrized-verification-of-distributed-cyber-physical-systems-a https://experts.illinois.edu/en/publications/parametrized-verification-of-distributed-cyber-physical-systems-a],
: [http://ieeexplore.ieee.org/document/6197398 http://ieeexplore.ieee.org/document/6197398],
: [http://dx.doi.org/10.1109/ICCPS.2012.24 http://dx.doi.org/10.1109/ICCPS.2012.24],
: [https://ieeexplore.ieee.org/document/6197398 https://ieeexplore.ieee.org/document/6197398],
: [http://www.taylortjohnson.com/bibtexbrowser.php?key=johnson2012iccps&bib=johnson_taylor_t.bib http://www.taylortjohnson.com/bibtexbrowser.php?key=johnson2012iccps&bib=johnson_taylor_t.bib],
: [https://academic.microsoft.com/#/detail/2149660990 https://academic.microsoft.com/#/detail/2149660990]

← Older revision	Revision as of 15:05, 3 February 2021
(No difference)

Johnson Mitra 2012a - Revision history

Scipediacontent: Scipediacontent moved page Draft Content 625578912 to Johnson Mitra 2012a

Scipediacontent: Created page with " == Abstract == In this paper, we present the formal modeling and automatic parameterized verification of a distributed air traffic control protocol called the Small Aircraft..."