Conference Papers

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

Browse

Subject: search.filters.subject.Fault Tree Analysis (FTA)

Search Results

Now showing 1 - 2 of 2
  • 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.
  • No Thumbnail Available
    Item
    Formal Specification and Verification of Time-Sensitive Drone Systems using TLA+: A Case Study
    (Institute of Electrical and Electronics Engineers Inc., 2024) Surya, A.; Ayush, V.; Thakur, V.; Nair, V.; Das, M.; Mohan, B.R.
    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.