Ural, H.,van der Schoot, Johannes J. M.2009-03-232009-03-2319991999Source: Dissertation Abstracts International, Volume: 60-08, Section: B, page: 4068.9780612387980http://hdl.handle.net/10393/8857http://dx.doi.org/10.20381/ruor-16026The research underlying this thesis concerns the verification of concurrent systems. In particular, strategies are studied to tackle the state explosion problem which arises during the verification of concurrent systems by state space exploration. State (space) exploration, commonly known also as reachability analysis, amounts to exploring in a systematic manner the entire state space of a system. One of the main causes of the state explosion problem in the verification of concurrent systems is the modeling of concurrency by the exploration of all possible interleavings of concurrent events/transitions. During reachability analysis, each possible way in which the execution of concurrent transitions can be ordered in time is examined. Several of the strategies proposed to relieve the state explosion problem in the verification of concurrent systems have proved promising indeed. This thesis contributes by proposing improvements of three existing relief strategies, namely fair reachability analysis, simultaneous reachability analysis and partial-order reduction methods. First, the technique of fair reachability analysis (FRA) is generalized from cyclic protocols to multi-cyclic protocols modeled as networks of communicating finite state machines (CFSMs). FRA is established as an effective and efficient relief strategy for the detection of deadlocks in multi-cyclic protocols with a finite fair reachable state space. It is also shown that FRA is infeasible as a relief strategy beyond the class of multi-cyclic protocols. Secondly, a technique called leaping reachability analysis (LRA) is presented as an incremental improvement of simultaneous reachability analysis (SRA), which was proposed as a relief strategy for the verification of logical correctness properties of protocols specified in the CFSM model without topological or structural constraints. LRA is proven to maintain the power of SRA to detect all deadlocks, all non-executable transitions, all unspecified receptions and all buffer overflows of the protocol. These analytical results are complemented by an empirical evaluation of the performance of LRA and SRA. Lastly, an enhancement of partial-order reduction methods is proposed for linear-time temporal logic (LTL) model-checking. More precisely, the concepts underlying LRA are integrated with those underlying partial-order reduction methods to enable further savings in both space and time for the verification of linear-time temporal properties of general, finite-state concurrent systems. This approach is subsequently fine-tuned for protocols specified in the CFSM model. (Abstract shortened by UMI.)198 p.Computer Science.Thesis