Improving state exploration techniques for the automatic verification 
of concurrent systems

Hans van der Schoot
PhD Thesis

University of Ottawa
1999

Abstract

The 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, i.e. all states 
and transitions of the system that can be reached from a given initial 
state. It is a simple and fully automatic technique that can be employed 
in principle to verify many different types of correctness requirements 
of concurrent systems, ranging from various general consistency 
requirements to more system-specific, functional requirements. However, 
the state explosion problem severely limits the applicability of 
reachability analysis in practice. The state spaces of most realistic 
industrial-strength systems are excessive in size (comprising hundreds 
of thousands or even millions of states and transitions), and thereby 
surpass any conceivable amount of memory and time available for analysis.

One of the main causes of the state explosion problem in the verification 
of concurrent systems is the modeling of concurrency by interleaving or, 
more accurately, 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. Yet, it has been recognized for quite some 
time that many interesting correctness properties of concurrent systems 
are insensitive to the interleaving order of concurrent transitions. 
Consequently, such systems often manifest a large number of reachable 
states and transitions that are redundant for verification purposes. For 
nearly two decades, this apprehension has inspired researchers to devise 
improved state exploration techniques that relieve the state explosion 
problem. These state exploration based relief strategies reduce the 
complexity of conventional reachability analysis by examining just part 
of the state space of a system, a part that is provably sufficient to 
verify one or several desirable properties. In effect, they enable the 
verification of concurrent systems without incurring (most of) the cost 
of modeling concurrency by interleaving.

Several of the strategies proposed to relieve the state explosion problem 
in the verification of concurrent systems have proved promising indeed, 
enabling in many cases substantial memory and time savings for state 
exploration. With the advent of these relief strategies, the 
applicability of verification by state exploration has thus certainly 
been widened to "larger" concurrent systems. Nevertheless, since 
concurrent systems are inherently complex and since this complexity is 
there to stay, pursuing further performance improvements in verification 
clearly remains of utmost importance. This thesis contributes by 
proposing improvements of three existing relief strategies, namely fair 
reachability analysis, simultaneous reachability analysis and partial-
order reduction methods. These are among the most evolved state 
exploration based relief strategies to date. First, the technique of fair 
reachability analysis (FRA) is generalized from cyclic to multi-cyclic 
protocols modeled as networks of communicating finite state machines 
(CFSMs). A multi-cyclic protocol constitutes one or more cyclic 
protocols, i.e. unidirectional rings, which are interconnected such that 
no two component cyclic protocols share more than one CFSM. 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 (i.e. the reduced state space of the protocol 
explored by FRA). Furthermore, 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. For any 
protocol in this model, 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, while enabling 
further reductions in the size of the state space that needs to be 
analyzed. These analytical results are complemented by an empirical 
evaluation of the performance of LRA and SRA, which reveals that LRA can 
indeed yield important extra savings in space and time over 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 (i.e. any system whose behavior can be 
defined as a finite transition system). This approach is subsequently 
fine-tuned for protocols specified in the CFSM model, whereby LRA emerges 
as an effective and uniform relief strategy for the verification of both 
logical (i.e. syntactic) and functional (i.e. semantic) correctness 
properties of protocols. Empirical results are provided which attest that 
the proposed approach to LTL model-checking is indeed a notable 
enhancement of the partial-order reduction approach.