Conference Papers

Permanent URI for this collectionhttps://idr.nitk.ac.in/handle/123456789/28506

Browse

Filters

20221

Settings

Author: search.filters.author.Guddeti, R.M.R.Subject: search.filters.subject.Fault Tree Analysis (FTA)

Search Results

Now showing 1 - 1 of 1
  • No Thumbnail Available
    Item
    Formal Specification and Verification of Drone System using TLA+: A Case Study
    (Institute of Electrical and Electronics Engineers Inc., 2022) Das, M.; Mohan, B.R.; Guddeti, R.M.R.
    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.