Research Commons
      • Browse 
        • Communities & Collections
        • Titles
        • Authors
        • By Issue Date
        • Subjects
        • Types
        • Series
      • Help 
        • About
        • Collection Policy
        • OA Mandate Guidelines
        • Guidelines FAQ
        • Contact Us
      • My Account 
        • Sign In
        • Register
      View Item 
      •   Research Commons
      • University of Waikato Theses
      • Masters Degree Theses
      • View Item
      •   Research Commons
      • University of Waikato Theses
      • Masters Degree Theses
      • View Item
      JavaScript is disabled for your browser. Some features of this site may not work without it.

      Partial Order Reduction with Compositional Verification

      Shaw, Adrian Mark
      Thumbnail
      Files
      thesis.pdf.pdf
      677.9Kb
      Citation
      Export citation
      Shaw, A. M. (2014). Partial Order Reduction with Compositional Verification (Thesis, Master of Science (MSc)). University of Waikato, Hamilton, New Zealand. Retrieved from https://hdl.handle.net/10289/9001
      Permanent Research Commons link: https://hdl.handle.net/10289/9001
      Abstract
      This thesis expands the usage of partial order reduction methods in reducing the state space of large models in model checking. The work done can be divided into two parts. In the first part we introduce two new ample conditions that utilise strongly connected components in place of two existing ample conditions that use cycles. We use these new conditions to optimise existing partial order reduction verifiers and extend them to verify nonblocking properties. We also introduce two selection strategies for choosing ample event sets and an improved ample algorithm in order to improve the efficiency of ample set computation, and investigate how the various combinations of these suggested algorithmic improvements effect several models of varying size. The second part of the thesis introduces the concept of using partial order reduction techniques in combination with compositional verification techniques. We introduce a modified version of the silent continuation rule that makes use of the independence relationship from partial order reduction methods and include algorithms by which they may be implemented in a model verifier. All of the original concepts developed in this thesis are also proven correct.
      Date
      2014
      Type
      Thesis
      Degree Name
      Master of Science (MSc)
      Supervisors
      Malik, Robi
      Publisher
      University of Waikato
      Rights
      All items in Research Commons are provided for private study and research purposes and are protected by copyright with all rights reserved unless otherwise indicated.
      Collections
      • Masters Degree Theses [2385]
      Show full item record  

      Usage

      Downloads, last 12 months
      27
       
       

      Usage Statistics

      For this itemFor all of Research Commons

      The University of Waikato - Te Whare Wānanga o WaikatoFeedback and RequestsCopyright and Legal Statement