Please use this identifier to cite or link to this item:
Full metadata record
|Bibliography: leaves 211-220
|xviii, 220 leaves : charts ; 30 cm.
|This thesis examines automated formal verification techniques and their associated space and time implementation complexity when applied to finite state concurrent systems. The focus is on concurrent systems expressed in the Communicating Sequential Processes (CSP) framework. An approach to the compilation of CSP system descriptions into boolean formulae in the form of Ordered Binary Decision Diagrams (OBDD) is presented, further utilised by a basic algorithm that checks a refinement or equivalence relation between a pair of processes in any of the three CSP semantic models. The performance bottlenecks of the basic refinement checking algorithms are identified and addressed with the introduction of a number of novel techniques and algorithms. Algorithms described in this thesis are implemented in the Adelaide Tefinement Checking Tool.
|Sequential processing (Computer science)
|Computer software Verification.
|Advances in space and time efficient model checking of finite state systems / Atanas Nikolaev Parashkevov.
|Dept. of Computer Science
|This electronic version is made publicly available by the University of Adelaide in accordance with its open access policy for student theses. Copyright in this thesis remains with the author. This thesis may incorporate third party material which has been used by the author pursuant to Fair Dealing exception. If you are the author of this thesis and do not wish it to be made publicly available or If you are the owner of any included third party copyright material you wish to be removed from this electronic version, please complete the take down form located at: http://www.adelaide.edu.au/legals.
|Thesis (Ph.D.)--University of Adelaide, Dept. of Computer Science, 2002
|Appears in Collections:
Files in This Item:
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.