Bibliography: leaves 211-220 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.
| Identifer | oai:union.ndltd.org:ADTP/120241 |
| Date | January 2002 |
| Creators | Parashkevov, Atanas. |
| Source Sets | Australiasian Digital Theses Program |
| Language | English |
| Detected Language | English |
| Relation | SUA |
Page generated in 0.0019 seconds