Return to search

Advances in space and time efficient model checking of finite state systems

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.

Identiferoai:union.ndltd.org:ADTP/120241
Date January 2002
CreatorsParashkevov, Atanas.
Source SetsAustraliasian Digital Theses Program
LanguageEnglish
Detected LanguageEnglish
RelationSUA

Page generated in 0.002 seconds