Show simple item record

dc.contributor.advisorStirling, Colin
dc.contributor.authorBruns, Glen R
dc.date.accessioned2004-03-03T09:51:08Z
dc.date.available2004-03-03T09:51:08Z
dc.date.issued1998-07
dc.identifier.urihttp://hdl.handle.net/1842/384
dc.description.abstractThe automatic verification of temporal properties of systems usually suffers from two problems. First, the size of the system that can be verified is very limited. Secondly, the results reflect only the behaviour of a system having particular parameters and initial conditions. Both problems are addressed by abstracting the system model relative to the property of interest. This thesis investigates two abstraction methods for processes. In the first method unary process operators serve as abstraction operations. We show that an abstract process satisfies a property expressed as a temporal logic formula just if the original process satisfies a transformed formula. We define various abstraction operators and illustrate their use in verification with examples. The method is also used to derive two well-known verification techniques. In the second method an abstract process and the original process are related by a process preorder. The weakly simulates and ready simulates preorders are used. For both we provide logical characterisations, abstraction operations, and algebraic laws. Our work differs from existing work on process abstraction in that we abstract process expressions directly and take account of the particular property to be verified. We show the practical value of our methods by using them to help verify properties of Dekker's mutual exclusion algorithm and Ben-Ari's concurrent garbage collection algorithm.en
dc.format.extent2139770 bytes
dc.format.mimetypeapplication/postscript
dc.language.isoen
dc.publisherUniversity of Edinburgh. College of Science and Engineering. School of Informatics.en
dc.titleProcess Abstraction in the Verification of Temporal Propertiesen
dc.typeThesis or Dissertation
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record