Formal Guarantees of Timely Progress for Distributed Knowledge Propagation
Open Access
- 21 October 2021
- journal article
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 348, 73-91
- https://doi.org/10.4204/eptcs.348.5
Abstract
Autonomous air traffic management (ATM) operations for urban air mobility (UAM) will necessitate the use of distributed protocols for decentralized coordination between aircraft. As UAM operations are time-critical, it will be imperative to have formal guarantees of progress for the distributed protocols used in ATM. Under asynchronous settings, message transmission and processing delays are unbounded, making it impossible to provide deterministic bounds on the time required to make progress. We present an approach for formally guaranteeing timely progress in a Two-Phase Acknowledge distributed knowledge propagation protocol by probabilistically modeling the delays using theories of the Multicopy Two-Hop Relay protocol and the M/M/1 queue system. The guarantee states a probabilistic upper bound to the time for progress as a function of the probabilities of the total transmission and processing delays being less than two given values. We also showcase the development of a library of formal theories, that is tailored towards reasoning about timely progress in distributed protocols deployed in airborne networks, in the Athena proof assistant.This publication has 50 references indexed in Scilit:
- Formalization of Measure Theory and Lebesgue Integration for Probabilistic Analysis in HOLACM Transactions on Embedded Computing Systems, 2013
- Reasoning about conditional probabilities in a higher-order-logic theorem proverJournal of Applied Logic, 2011
- The Heard-Of model: computing in distributed systems with benign faultsDistributed Computing, 2009
- Formal verification of tail distribution bounds in the HOL theorem proverMathematical Methods in the Applied Sciences, 2008
- Formalization of the Standard Uniform random variableTheoretical Computer Science, 2007
- Modeling and Verification of Reliable Messaging by Graph Transformation SystemsElectronic Notes in Theoretical Computer Science, 2007
- The perfectly synchronized round-based model of distributed computingInformation and Computation, 2006
- Hazard criteria for wake vortex encounters during approachAerospace Science and Technology, 2004
- Mobility increases the capacity of ad hoc wireless networksIEEE/ACM Transactions on Networking, 2002
- Time Bounds for Decision Problems in the Presence of Timing Uncertainty and FailuresJournal of Parallel and Distributed Computing, 2001