Please use this identifier to cite or link to this item:
Full metadata record
DC FieldValueLanguage
dc.contributor.authorParashkevov, Atanasen
dc.descriptionBibliography: leaves 211-220en
dc.descriptionxviii, 220 leaves : charts ; 30 cm.en
dc.description.abstractThis 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.en
dc.format.extent176529 bytesen
dc.subject.lcshSequential processing (Computer science)en
dc.subject.lcshComputer software Verification.en
dc.titleAdvances in space and time efficient model checking of finite state systems / Atanas Nikolaev Parashkevov.en
dc.contributor.schoolDept. of Computer Scienceen
dc.provenanceThis 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:
dc.description.dissertationThesis (Ph.D.)--University of Adelaide, Dept. of Computer Science, 2002en
Appears in Collections:Research Theses

Files in This Item:
File Description SizeFormat 
01front.pdf 172.39 kBAdobe PDFView/Open
02whole.pdf12.78 MBAdobe PDFView/Open

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.