Show simple item record  

dc.contributor.advisorMalik, Robi
dc.contributor.authorShaw, Adrian Mark
dc.date.accessioned2014-12-16T03:10:04Z
dc.date.available2014-12-16T03:10:04Z
dc.date.issued2014
dc.identifier.citationShaw, 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/9001en
dc.identifier.urihttps://hdl.handle.net/10289/9001
dc.description.abstractThis 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.
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.publisherUniversity of Waikato
dc.rightsAll items in Research Commons are provided for private study and research purposes and are protected by copyright with all rights reserved unless otherwise indicated.
dc.subjectPartial order reduction
dc.subjectModel checking
dc.subjectcompositional verification
dc.titlePartial Order Reduction with Compositional Verification
dc.typeThesis
thesis.degree.grantorUniversity of Waikato
thesis.degree.levelMasters
thesis.degree.nameMaster of Science (MSc)
dc.date.updated2014-06-27T03:25:48Z
pubs.place-of-publicationHamilton, New Zealanden_NZ


Files in this item

This item appears in the following Collection(s)

Show simple item record