Formal Proof and Performance Testing of the Unmanned Vehicle System Logging Protocol
Abstract
Multivehicle autonomous systems are becoming increasingly relevant, but the loss of individual vehicles and unstable communications environments make maintenance of data logs for mission reconstruction and analysis difficult. A blockchain-based distributed ledger protocol, the Unmanned Vehicle System Logging Protocol (UVSLP), has been proposed to address this problem. Formal proofs of its correctness and controlled experiments examining its performance are required to use the proposed protocol with higher confidence. This work documents the formal definition of the protocol using predicate logic with added temporal operators and provides formal proofs of the protocol's claimed properties. In addition, we use a prototype implementation in a simulated environment to characterize the protocol's performance for specific network loss rate, event generation rate, and number of vehicles values. Results are presented in the form of number of messages and volume of data produced by the protocol for each configuration. Our results show that message volume increases no worse than linearly as the number of vehicles and event generation rates increase and decreases as network loss rates increase. The culmination of this thesis is a mathematically proven protocol with known performance characteristics that improves the resiliency and availability of drone swarm data.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 2023
- Accession Number
- AD1224640
Entities
People
- Dalton L. Duvio
Organizations
- Naval Postgraduate School