Formal Specification and Verification of Drone System using TLA+: A Case Study
No Thumbnail Available
Date
2022
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Institute of Electrical and Electronics Engineers Inc.
Abstract
A Safety-Critical System is a System whose break-down may cause disastrous effects to the environment, damage the system, or cause loss of life. Sometimes loss or misuse of information can indirectly cause harmful impacts due to system failure. In this paper, we study the various components of a drone system and analyze the safety of this Safety-Critical System (SCS) by looking into the potential failure using Fault Tree Analysis (FTA). Drone system failure or crash has been specified and verified using the Temporal Logic of Actions (TLA+) tool. The TLA+ tool consists of mathematical notations to describe the system specification using discrete mathematical concepts or formal methods. We tried to build a TLA+ Specification and Verification for this drone system, parse it using the TLC model checker successfully, and observed the final number of states to justify the correctness of the specification. © 2022 IEEE.
Description
Keywords
Fault Tree Analysis (FTA), Safety-Critical System (SCS), Temporal Logic Of Actions (TLA+) tool, TLC Model Checker
Citation
Proceedings - 2022 IEEE/ACIS 24th International Winter Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing, SNPD 2022, 2022, Vol., , p. 156-161