Loading...

Compositional Verification of Timed Distributed Systems

Moeini Jam, Mehran | 2024

78 Viewed
  1. Type of Document: M.Sc. Thesis
  2. Language: Farsi
  3. Document No: 57160 (19)
  4. University: Sharif University of Technology
  5. Department: Computer Engineering
  6. Advisor(s): Movaghar Rahimabadi, Ali
  7. Abstract:
  8. Society is becoming increasingly dependent on computer systems, raising a somewhat neglected but vital question: Are these systems as safe as we think they are? To address this concern, many approaches have emerged alongside the testing process to enhance the reliability of our systems. One of the most successful approaches involves viewing computer systems as mathematical objects and making assertions about their intended behavior. Formal verification is the act of attempting to establish the truth of these statements and ensure the safe behavior of the system. Model Checking is a mainstream formal verification technique that has proven its usability in verifying complex software and hardware systems. However, a significant obstacle remains unsolved: the often enormous size of the state space of the system under consideration, a phenomenon called state-space explosion. To address this problem, considerable efforts have been dedicated to devising viable solutions. This thesis is based on one of these techniques, called compositional verification, which involves decomposing the system into two or more components and deducing the satisfaction or refutation of the desired property from these smaller, more compact components. To the best of our knowledge, aside from a recent paper employing a learning approach, no other endeavors have been made to leverage assume-guarantee reasoning—the predominant compositional technique—to address systems modeled as general timed automata. In this thesis, for the first time, we propose a non-learning algorithm for assume-guarantee verification of timed systems modeled as deterministic timed automata and a wide class of non-deterministic timed automata with multiple clocks. We prove the soundness of our method and incorporate it in analyzing a case study. We conclude with some suggestions for future work
  9. Keywords:
  10. Formal Verification ; Model Cheking ; Distributed System ; Timed Systems ; Compositional Verification

 Digital Object List

 Bookmark

...see more