Formal Techniques for Realizability Checking and Synthesis of Infinite-State Reactive Systems
2020-07
Loading...
View/Download File
Persistent link to this item
Statistics
View StatisticsJournal Title
Journal ISSN
Volume Title
Title
Formal Techniques for Realizability Checking and Synthesis of Infinite-State Reactive Systems
Authors
Published Date
2020-07
Publisher
Type
Thesis or Dissertation
Abstract
Reactive systems are fundamental building blocks in the development of critical safety systems. The are called "reactive" due to the necessity of them interacting with (or against) an unpredictable and uncontrollable environment, for an indefinite amount of time. As a consequence, the verification of a critical system more often than not in- volves the process of writing requirements, modeling, implementing and testing reactive subcomponents. Research in formal verification for reactive systems attempts to solve fundamental problems in each of these processes, with an emphasis given on the cre- ation of mathematical proofs regarding the system's safety. More importantly, it has been shown that such proofs can lead to significant savings both in development time as well as overall production cost. This dissertation explores the problem of reactive synthesis, where the goal is the development of decision procedures that are able to (dis)prove the realizability of reactive system specifications, as well as produce artifacts that essentially serve as witnesses to the decision. Reactive synthesis is a problem closely related to formal verification, as it requires the development of precise, mathematical proofs of realizability. The overwhelming majority of research conducted in this area has so far been focused in its application to propositional specification, where only operations over the Boolean domain can be performed. For the first part of this thesis, we propose novel, efficient reactive synthesis algorithms that extend the support for propositional specification to also generate implementations when the requirements involve the use of richer theories, such as integer and real arithmetic. We discuss the advantages and disadvantages of each algorithm, and accompany their implementation with a formal proof of soundness. In the second part of this dissertation, we delve into an unexplored sub-problem in reactive iv synthesis, where we present the first attempt ever to synthesize witnesses for infinite-state problems in which the implementation behaves in a random, diverse manner. While the product of synthesis is typically expected to be a deterministic witness, we argue that randomness can still be valuable in practice. To that end, we evaluate the application of randomly-behaving solutions to problems related to fuzz testing and robot motion planning, demonstrating how reactive synthesis can be used in an innovative way in software engineering concepts that have not been considered before.
Description
University of Minnesota Ph.D. dissertation.July 2020. Major: Computer Science. Advisors: Michael Whalen, Mats Heimdahl. 1 computer file (PDF); 154 pages.
Related to
Replaces
License
Collections
Series/Report Number
Funding information
Isbn identifier
Doi identifier
Previously Published Citation
Suggested citation
Katis, Andreas. (2020). Formal Techniques for Realizability Checking and Synthesis of Infinite-State Reactive Systems. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/216377.
Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.