Formal Specification and Verification of Time-Sensitive Drone Systems using TLA+: A Case Study

Abstract

This research paper presents a detailed analysis of time sensitivity in drone system operations, exploring the critical impact of temporal factors on their performance and reliability using Temporal Logic of Action (TLA+), primarily aiming to enhance the reliability and safety of drone systems. The study addresses the critical need to rigorously model complex drone behaviors while considering their interactions with the environment to identify and rectify potential safety hazards and system flaws. It introduces a new dimension by emphasizing the temporal aspect in critical systems, providing a dynamic perspective on system reliability. This research introduces a real-time module to accommodate commonly used time patterns, responding to the growing demand for time-sensitive evaluations in mission-critical systems. © 2024 IEEE.