Under consideration for publication in Formal Aspects of Computing

Concurrent Software Verification with
States, Events, and Deadlocks1,2
Sagar Chaki1 , Edmund Clarke2 , Joël Ouaknine3 , Natasha Sharygina1,2 , Nishant Sinha2
1 Software Engineering Institute, Carnegie Mellon University, Pittsburgh, USA
2 Computer Science Department, Carnegie Mellon University, Pittsburgh, USA
3 Oxford University Computing Laboratory, Oxford, UK

Abstract. We present a framework for model checking concurrent software systems which incorporates
both states and events. Contrary to other state/event approaches, our work also integrates two powerfulverification techniques, counterexample-guided abstraction refinement and compositional reasoning. Our
specification language is a state/event extension of linear temporal logic, and allows us to express many
properties of software in a concise and intuitive manner. We show how standard automata-theoretic LTLmodel checking algorithms can be ported to our framework at no extra cost, enabling us to directly benefit
from the large body of research on efficient LTL verification.
We also present an algorithm to detect deadlocks in concurrent message-passing programs. Deadlockfreedom is not only an important and desirable property in its own right, but is also a prerequisite for thesoundness of our model checking algorithm. Even though deadlock is inherently non-compositional and is
not preserved by classical abstractions, our iterative algorithm employs both (non-standard) abstractions
and compositional reasoning to alleviate the state-space explosion problem. The resulting framework differs
in key respects from other instances of the counterexample-guided abstraction refinement paradigm foundin the literature.
We have implemented this work in the magic verification tool for concurrent C programs and performed
tests on a broad set of benchmarks. Our experiments show that this new approach not only eases thewriting of specifications, but also yields important gains both in space and in time during verification. In
certain cases, we even encountered specifications that could not be verified using traditional pure eventbased or state-based approaches, but became tractable within our state/event framework. We also recorded
substantial reductions in time and memory consumption when performing deadlock-freedom checks with
our new abstractions. Finally, we report two bugs (including a deadlock) in the source code of Micro-C/OS
versions 2.0 and 2.7, which we discovered during our experiments.
Keywords: Concurrent software; Model checking; Temporal logic; States and events; Deadlock; Compositional reasoning; Counterexample-guided abstraction refinement

1 This research was sponsored by the National Science Foundation (NSF) under grants no. CCR-9803774 and CCR-0121547,
the Office of Naval Research (ONR) and the Naval Research Laboratory (NRL) under contract no. N00014-01-1-0796, the Army
Research Office (ARO) under contract no. DAAD19-01-1-0485, and was conducted as part of the Predictable Assembly from
Certifiable Components (PACC) project at the Software Engineering Institute (SEI).
2 This article combines and builds upon the papers [CCO + 04] and [CCOS04].
Correspondence and offprint requests to: Joël Ouaknine, joel@comlab.ox.ac.uk.

2Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha

1. Introduction
Control systems ranging from smart cards to automated flight controllers are increasingly being incorporated
within complex software systems. In many instances, errors in such systems can have dramatic consequences,hence the need to be able to ensure and guarantee their correctness.
In this endeavour, the well-known methodology of model checking [CE81, CES86, QS81, CGP99] holds
much promise. Although most of its early applications dealt with hardware and communication protocols, model checking is increasingly used to verify software systems [SLAM, BR01, BMMR01, BLAST,HJMS02, HJMQ03, CDH+ 00, PDV01, Sto02, MAGIC, CCG+ 03, COYC03, AQR+ 04]. Unfortunately, applying model checking to software is complicated by several factors, ranging from the difficulty to modelcomputer programs—due to the complexity of programming languages as compared to hardware description
languages—to difficulties in specifying meaningful properties of software using the usual temporal logicalformalisms of model checking. A third reason is the perennial state-space explosion problem, whereby thecomplexity of verifying an implementation against a specification becomes prohibitive.
The most common instantiations of model checking to date have focused on finite-state models and either
branching-time (CTL [CE81]) or linear-time (LTL [LP85]) temporal logics. To apply model checking to software, it is necessary to specify (often complex) properties on the finite-state abstracted models of computer
programs. The difficulties in doing so are even more pronounced when reasoning about modular software,such as concurrent or component-based sequential programs. Indeed, in modular programs, communication
among modules proceeds via events (or actions), which can represent function calls, requests and acknowledgements, etc. Moreover, such communication is commonly data-dependent. Software behavioural claims,
therefore, are often specifications defined over combinations of program events and data valuations.
Existing modelling techniques usually represent finite-state machines as finite annotated directed graphs,
using either state-based or event-based formalisms. Although both frameworks are interchangeable (an event
can be encoded as a change in state variables, and likewise one can equip a state with different events toreflect different values of its internal variables), converting from one representation to the other often leads
to a significant enlargement of the state space. Moreover, neither approach on its own is practical whenit comes to modular software, in which events are often data-dependent: considerable domain expertise isusually required to annotate the program and to specify proper claims.
In this work, we propose a framework in which both state-based and event-based properties can be expressed, combined, and verified. The modelling framework consists of labelled Kripke structures (LKS), which
are directed graphs in which states are labelled with atomic propositions and transitions are labelled with
events. The specification logic is a state/event derivative of LTL. This allows us to represent both software
implementations and specifications directly without any program annotations or privileged insights into program execution. We further show that standard efficient LTL model checking algorithms can be applied,at no extra cost in space or time, to help reason about state/event-based systems. We have implemented
our approach within the concurrent C verification tool magic [MAGIC, CCG+ 03, COYC03], which extracts
LKS models from C programs automatically via predicate abstraction [GS97]. We report promising resultsin the large set of benchmarks that we have tackled.
A core feature of magic is the use of compositional abstraction refinement techniques developed for theefficient verification of concurrent software [COYC03]. These techniques are embedded within a counterexample-guided abstraction refinement framework (CEGAR for short) [CGJ+ 00]. CEGAR lets us investigate
the validity of a given specification through a sequence of increasingly refined abstractions of our system, until
the property is either established or a real counterexample is found. Moreover, thanks to compositionality,
the abstraction, counterexample validation, and refinement steps can all be carried out component-wise,
thereby alleviating the need to build the full state space of the distributed system.
The verification of state/event specifications on concurrent LKSs as described above requires, in order
to be sound, that the global composed system be deadlock-free. When several components communicate
via blocking message-passing, the possibility that two components might at some point have incompatible
communication requirements can unfortunately in general not be discounted. Indeed, such an occurrence istermed deadlock and results in a situation in which no further progress can be made. Deadlock-freedom isoften a vital specification in its own right, especially for safety-critical systems, such as embedded systems
or plant controllers, that are expected always to service requests within a fixed time limit or be responsive
to external stimuli.
Unfortunately, deadlock is inherently non-compositional and moreover is not preserved by classical existential or universal abstractions. One of the main contributions of this paper is the development of new,Concurrent Software Verification with States, Events, and Deadlocks

3

non-standard abstraction schemes that do preserve deadlock and are (in an appropriate sense) compositional.
These abstractions are inspired from the notion of failures in the process algebra CSP [Hoa85, Ros97]. As
a result, we have been able to devise a compositional CEGAR-based framework for deadlock detection,
which has led to substantial time and space improvements over corresponding classical approaches found in
the literature: our magic implementation recorded speed-ups of up to 20 times along with up to four-fold
reductions in memory usage in some of our benchmarks.
We carried out a large number of experiments to evaluate both our state/event model checking algorithm
as well as our deadlock detection scheme. Our benchmarks were for the most part derived from (i) OpenSSL0.9.6c, an open-source implementation of the SSL protocol; (ii) IPC-1.6, an inter-process communication
protocol developed by ABB used to mediate information in a multi-threaded robotics control automation
system; and (iii) Micro-C/OS 2.0 and 2.7, a real-time operating system for embedded applications. In thecase of the latter, we discovered and report two bugs (including a deadlock), which have been acknowledgedby the implementors of Micro-C/OS.
The rest of this article is organized as follows. In Section 2 we summarize related work. Section 3 introduces our state/event implementation formalism, labelled Kripke structures. We also discuss existential
abstractions, parallel composition, and assorted results. This is followed by Section 4 in which we present ourstate/event temporal logic. We review standard automata-theoretic model checking techniques, and show
how these can be adapted to this new framework. In Section 5, we illustrate these ideas by modelling asimple surge protector. We then contrast our approach with pure state-based and event-based alternatives,and show that both the resulting implementations and specifications are significantly more cumbersome. We
then use magic to check these specifications, and discover that the non-state/event formalisms incur important time and space penalties during verification. Section 6 details our compositional CEGAR algorithm
for model checking state/event specifications on labelled Kripke structures, and integrates as a whole thevarious pieces presented in earlier sections.
Deadlock is formally introduced in Section 7. We then explain why classical abstractions are inadequate
for handling deadlock in Section 8, and propose new abstractions that overcome the problems raised. Section 9
explains how these abstractions can be exploited within a compositional CEGAR framework, culminatingin our deadlock detection algorithm. Finally, Section 10 is devoted to experiments and case studies, while
Section 11 concludes and discusses future work.

2. Related Work
The formalization of a general notion of abstraction first appeared in [CC77]. The abstractions used in our
approach are conservative: they are guaranteed to preserve ‘undesirable’ properties of the system, so that
if the abstraction is bug-free then so is the original model, but may introduce spurious ‘bad’ behaviours
not present in the original system—for more details on conservative abstractions, see, e.g., [Kur89, CGL94].
Conservative abstractions usually lead to significant reductions in the state space but in general require an
iterated abstraction refinement mechanism (see below) in order to establish specification satisfaction.
Counterexample-guided abstraction refinement [Kur94, CGJ+ 00], or CEGAR, is an iterative procedure
whereby spurious counterexamples to a specification are repeatedly eliminated through incremental refinements of a conservative abstraction of the system. CEGAR has been used, among others, in [NCOD97] (innon-automated form), and [BR01, PDV01, LBBO01, HJMS02, CCK+ 02, CGKS02, COYC03].
Compositionality, which features centrally in our work, is broadly concerned with the preservation ofproperties under substitution of components in concurrent systems. It has been extensively studied, among
others, in process algebra (e.g., [Hoa85, Mil89, Ros97]), in temporal logic model checking [GL94], and in theform of assume-guarantee reasoning [McM97, HQR00, CGP03].
The combination of CEGAR and compositional reasoning is a relatively new approach. In [BLO98],
a compositional framework for (non-automated) CEGAR over data-based abstractions is presented. Thisapproach differs from ours in that communication takes place through shared variables (rather than blocking
message-passing), and abstractions are refined by eliminating spurious transitions, rather than by splitting
abstract states.
The idea of combining state-based and event-based formalisms is certainly not new. De Nicola andVaandrager [NV95], for instance, introduce ‘doubly labelled transition systems’, which are very similar to
our LKSs. From the specification point of view, our state/event version of LTL is also subsumed by the modal
mu-calculus [Koz83, Pnu86, BS01], via a translation of LTL formulas into Büchi automata. The novelty of4

Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha

our approach, however, is the way in which we efficiently integrate an expressive state/event formalism withpowerful verification techniques, namely CEGAR and compositional reasoning. We are able to achieve this
precisely because we have adequately restricted the expressiveness of our framework. To our knowledge, ourwork is the first to combine these three features within a single setup.
Kindler and Vesper [KV98] propose a state/event-based temporal logic for Petri nets. They motivate
their approach by arguing, as we do, that pure state-based or event-based formalisms lack expressiveness inimportant respects.
Huth et al. [HJS01] also propose a state/event framework, and define rich notions of abstraction andrefinement. In addition, they provide ‘may’ and ‘must’ modalities for transitions, and show how to perform
efficient three-valued verification on such structures. They do not, however, provide an automated CEGAR
framework, and it is not clear whether they have implemented and tested their approach.
Giannakopoulou and Magee [GM03] define ‘fluent’ propositions within a labelled transition systems
context to express action-based linear-time properties. A fluent proposition is a property that holds after
it is initiated by an action and ceases to hold when terminated by another action. Their work exploits
partial-order reduction techniques and has been implemented in the LTSA tool [LTSA].
In a comparatively early paper, De Nicola et al. [NFGR93] propose a process algebraic framework withan action-based version of CTL as specification formalism. Verification then proceeds by first translating theunderlying labelled transition systems (LTSs) of processes into Kripke structures and the action-based CTL
specifications into equivalent state-based CTL formulas. At that point, a model checker is used to establish
or refute the property.
Dill [Dil88] defines ‘trace structures’ as algebraic objects to model both hardware circuits and their
specifications. Trace structures can handle equally well states or events, although usually not both at thesame time. Dill’s approach to verification is based on abstractions and compositional reasoning, albeit without
an iterative counterexample-driven refinement loop.
In general, events (input signals) in circuits can be encoded via changes in state variables. Browne makes
use of this idea in [Bro89], which features a CTL∗ specification formalism. Browne’s framework also features
abstractions and compositional reasoning, in a manner similar to Dill’s.
Burch [Bur92] extends the idea of trace structures into a full-blown theory of ‘trace algebra’. The focus
here however is the modelling of discrete and continuous time, and the relationship between these twoparadigms. His work also exploits abstractions and compositionality, however once again without automatedcounterexample-guided refinements.
Deadlock detection has been widely studied in various contexts. One of the earliest deadlock-detection
tools, for the process algebra CSP, was FDR [FSEL]; see also [RD87, BR91, MJ97, Ros97, MH00]. Corbett
has evaluated various deadlock-detection methods for concurrent systems [Cor96] while Demartini et al.
have developed deadlock-detection tools for concurrent Java programs [DIS99]. However, to the best of ourknowledge, none of these approaches involve abstraction refinement or compositionality in automated form.
Very recently, the notion of stuck-freedom [FHRR04], closely related to deadlock-freedom, has beendeveloped for the process algebra CCS. Stuck-freedom is compositional and an algorithm for model checking
stuck-free conformance for concurrent software has been implemented in the tool zing [AQR + 04].

3. Labelled Kripke Structures
A labelled Kripke structure (LKS for short) is a 7-tuple (S, Init, P, L, T, Σ, E) with S a finite set of states,
Init ⊆ S a set of initial states, P a finite set of atomic state propositions, L : S → 2 P a state-labelling function,
T ⊆ S × S a transition relation, Σ a finite set (alphabet) of events (or actions), and E : T → (2 Σ \ {∅}) aAtransition-labelling function. We often write s −→ s0 to mean that (s, s0 ) ∈ T and A ⊆ E(s, s0 ).3 In case A isa{a}a singleton set {a} we write s −→ s0 rather than s −→ s0 . Note that T and E are entirely determined by theacollection of transitions of the form s −→ s0 . Note also that both states and transitions are ‘labelled’, theformer with sets of atomic propositions, and the latter with non-empty sets of events.
We do not assume that the transition relation is total, and indeed we will see that the possibility ofdeadlock (reaching a state with no successor) is an unavoidable consequence of the blocking message-passing
3

In keeping with standard mathematical practice, we write E(s, s0 ) rather than the more cumbersome E((s, s0 )).

Concurrent Software Verification with States, Events, and Deadlocks

5

semantics we have chosen to model concurrency. We are, however, mainly interested in non-deadlocking
behaviour, and an algorithm to detect deadlock is presented in Section 9.
A path π = hs1 , a1 , s2 , a2 , . . .i of an LKS is an alternating sequence of states and events subject to theaifollowing: for each i > 1, si ∈ S, ai ∈ Σ, and si −→si+1 . Paths can be infinite or finite, however we requirethat a finite path end with a state (rather than with an event). We usually assume that a path is infinite
unless specified otherwise. Note that finite paths are not required to be ‘maximal’.
Given an LKS M , we write Path(M ) to denote the set of infinite paths of M whose first state lies inthe set Init of initial states of M . Later on, we will also write FPath(M ) to denote the collection of finite
Init-rooted paths of M .
Intuitively, an LKS M represents a finite-state model of some program. States correspond to program
statements, and atomic state propositions correspond to predicates on the local variables of the program,or to any other property we may wish to record of a given state. States are then labelled with precisely
all of the atomic propositions that they satisfy. Upon moving from one state to another, we assume that
the LKS performs some visible event, for potential synchronous communication purposes with another concurrent component (LKS). The LKS may offer several distinct events—corresponding to distinct offers ofsynchronization—only one of which will be performed at any one time; for this reason, transitions are labelledwith non-empty sets of events.
We are mainly interested in modelling reactive systems and components intended to run indefinitely, suchas file servers or operating systems, hence our primary focus on infinite paths. Of course, systems with awell-defined notion of termination, such as authentication protocols, can also be handled in our framework,by modelling termination as a transition to a special ‘sink’ state, from which only self-transitions are possible.

3.1. Abstraction
The notion of abstraction is central to our approach. We list below the properties that we require of any
abstraction scheme to be usable in our framework, and then give a concrete method for constructing abstractions that meet these criteria in the next subsection.
In general, given an LKS M , we want an abstraction of M to be conservative, i.e., to over-approximate,in a controlled manner, the behaviours of M . We want the abstraction to adequately reflect the events that
M can perform, but we may only be interested in a specific subset of the atomic state propositions of M ,and consequently require the abstraction to faithfully reflect only those state propositions that belong tothis subset.
Let M = (S, Init, P, L, T, Σ, E) and A = (SA , Init A , PA , LA , TA , ΣA , EA ) be two LKSs. We say that A isan abstraction of M , written M v A, iff
1. PA ⊆ P ,2. ΣA = Σ, and3. For every path π = hs1 , a1 , . . .i ∈ Path(M ) there exists a path π 0 = hs01 , a01 , . . .i ∈ Path(A) such that, foreach i > 1, a0i = ai and LA (s0i ) = L(si ) ∩ PA .
The set PA of atomic state propositions of the abstraction is the subset of state propositions of M that
we are interested in. An important special case is when PA = ∅, in which case we really are only interested
in the sequences of events that M can perform—this will be useful when dealing with deadlock detection
later on.
Note that this paper focuses on linear-time behaviours, and hence our abstractions are defined in termsof paths rather than trees. For a branching-time account of concurrent software verification, we refer thereader to [CCG+ 05].
Two-way abstraction defines an equivalence relation ∼ on LKSs: M ∼ M 0 iff M v M 0 and M 0 v M . We
shall only be interested in LKSs up to ∼-equivalence (see Proposition 3 in Section 4).

3.2. Existential Quotients of Labelled Kripke Structures
We present a specific method for constructing abstractions that meet the criteria laid out above. An abstraction of an LKS M is obtained by quotienting the states of M by a suitable equivalence relation. The idea

6

Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha

is very similar to the well-known notion of ‘existential abstraction’ for ordinary Kripke structures in which
certain variables are hidden [CGJ+ 00].
More precisely, for M = (S, Init, P, L, T, Σ, E), let PA ⊆ P be a subset of atomic state propositions of M ,and let ≈ be an equivalence relation on the states S of M that respects PA : if s ≈ s0 , then L(s)∩PA = L(s0 )∩PA . The existential quotient of M (with respect to PA and ≈) is the LKS A = (SA , Init A , PA , LA , TA , ΣA , EA )such that:
1. SA = S/≈, the collection of equivalence classes of S,
2. Init A = {[s] ∈ S/≈ | ∃s0 ∈ [s]  s0 ∈ Init},
3. for all s ∈ S, LA ([s]) = L(s) ∩ PA ,4. ΣA = Σ, andaa5. for all s, s0 ∈ S and a ∈ Σ, [s1 ] −→ [s2 ] iff there exists s01 ∈ [s1 ], s02 ∈ [s2 ] such that s01 −→ s02 .
We write M/(PA , ≈) or even M/≈ (when the set PA is clearly understood from the context) to denotethe abstraction A of M obtained in the above manner. The main advantage of working with M/≈ is that ingeneral it has a smaller state space than M .
We now have:
Proposition 1. For M an LKS, any existential quotient M/(PA , ≈) of M is a genuine abstraction of M inthe sense of Subsection 3.1: M v M/(PA , ≈).
In fact, one can show that any abstraction M/(PA , ≈) of M simulates M , so that existential quotientsare branching-time abstractions as well as linear-time abstractions; we will not, however, make use of thisfact in this paper.
Note that any PA -respecting equivalence relation ≈ on the state space of M can be viewed as a partitionof this state space. Moreover, since any refinement (sub-partition) of a P A -respecting partition is again
PA -respecting, we have:
Proposition 2. Let M be an LKS and let M/(PA , ≈) be an abstraction of M . For any refinement ≈0 of thepartition ≈, M/(PA , ≈0 ) is an abstraction of M that is also a refinement of M/(PA , ≈): M v M/(PA , ≈0 ) v
M/(PA , ≈).
We leave the straightforward proofs of Propositions 1 and 2 to the reader.

3.3. Parallel Composition
The notion of parallel composition that we consider in this paper allows for communication through shared
events only; in particular, we forbid the sharing of variables. This restriction facilitates the use of compositional reasoning in verifying specifications.
Let M1 = (S1 , Init 1 , P1 , L1 , T1 , Σ1 , E1 ) and M2 = (S2 , Init 2 , P2 , L2 , T2 , Σ2 , E2 ) be two LKSs. Assume that
M1 and M2 are compatible, i.e., that they do not share states or variables: S1 ∩S2 = P1 ∩P2 = ∅. The parallel
composition of M1 and M2 is given by M1 k M2 = (S1 × S2 , Init 1 × Init 2 , P1 ∪ P2 , L1 ∪ L2 , T, Σ1 ∪ Σ2 , E),A
where (L1 ∪ L2 )(s1 , s2 ) = L1 (s1 ) ∪ L2 (s2 ), and T and E are such that (s1 , s2 ) −→ (s01 , s02 ) iff A 6= ∅ and oneof the following holds:
A

1. A ⊆ Σ1 \ Σ2 and s1 −→ s01 and s02 = s2 ,A

2. A ⊆ Σ2 \ Σ1 and s2 −→ s02 and s01 = s1 ,A

A

3. A ⊆ Σ1 ∩ Σ2 and s1 −→ s01 and s2 −→ s02 .
In other words, components must synchronize on shared actions and proceed independently on local
actions. Moreover, local variables are preserved by the respective states of each component. This notion ofparallel composition is derived from CSP [Hoa85, Ros97]; see also [ACFM85].
Note that, because of our blocking semantics for parallel composition, it is possible for M 1 k M2 to exhibit
deadlock—i.e., reach some state with no outgoing transition—even if both M 1 and M2 are deadlock-free.
Deadlock arises through incompatible communication requirements: for example, one component might be
waiting for some input or acknowledgement that the other component is incapable of supplying. In that case

Concurrent Software Verification with States, Events, and Deadlocks

7

the two components are stuck and cannot make any further progress. Deadlock is clearly an undesirable
behaviour and is usually symptomatic of a bug in the program.
Let M1 and M2 be as above, and let π = h(s11 , s21 ), a1 , . . .i be an alternating infinite sequence of statesand events of M1 k M2 . The projection πMi of π on Mi consists of the (possibly finite) subsequence of/ Σi . In other words, we keep fromhsi1 , a1 , . . .i obtained by simply removing all pairs haj , sij+1 i for which aj ∈π only those states that belong to Mi , and excise any transition labelled with an event not in Mi ’s alphabet.
We now record the following theorem, which extends similar standard results for the process algebra CSP(for related proofs, we refer the reader to [Ros97]).
Theorem 1.
1. Parallel composition is associative and commutative up to ∼-equivalence. Thus, in particular, no bracketing is required when combining more than two LKSs.
2. Let M1 , . . . , Mn be compatible LKSs, and let A1 , . . . , An be respective abstractions of the Mi : for eachi, Mi v Ai . Then M1 k . . . k Mn v A1 k . . . k An . In other words, parallel composition preserves theabstraction relation.
3. Let M1 , . . . , Mn be compatible LKSs with respective alphabets Σ1 , . . . , Σn , and let π be an infinite
alternating sequence of states and events of the composition M1 k . . . k Mn . Then π ∈ Path(M1 k . . . k
Mn ) iff, for each i, there exists πi0 ∈ Path(Mi ) such that πMi is a prefix4 of πi0 . In other words, whether
a path belongs to the language of a parallel composition of LKSs can be checked by projecting andexamining the path on each individual component separately.
Theorem 1 forms the basis of our compositional approach to verification: abstraction, counterexample
validation, and refinement can all be done component-wise.

4. State/Event Linear Temporal Logic
We now present a logic enabling us to refer easily to both states and events when constructing specifications.
Given an LKS M = (S, Init, P, L, T, Σ, E), we consider linear temporal logic state/event formulas overthe sets P and Σ (here p ranges over P and a ranges over Σ):
φ ::= p | a | ¬φ | φ ∧ φ | Xφ | Gφ | Fφ | φ U φ.
We write SE-LTL to denote the resulting logic, and in particular to distinguish it from (standard) LTL.
Let π = hs1 , a1 , s2 , a2 , . . .i be an infinite path. Let π i stand for the suffix of π starting in state si . We
then inductively define path-satisfaction of SE-LTL formulas as follows:
1. π  p iff s1 is the first state of π and p ∈ L(s1 ),2. π  a iff a is the first event of π,
3. π  ¬φ iff π 2 φ,
4. π  φ1 ∧ φ2 iff π  φ1 and π  φ2 ,5. π  Xφ iff π 2  φ,
6. π  Gφ iff, for all i > 1, π i  φ,
7. π  Fφ iff, for some i > 1, π i  φ, and8. π  φ1 U φ2 iff there is some i > 1 such that π i  φ2 and, for all 1 6 j 6 i − 1, π j  φ1 .
We then let M  φ iff, for every infinite path π ∈ Path(M ), π  φ.
Let us also introduce the derived W operator: φ1 W φ2 iff (Gφ1 ) ∨ (φ1 U φ2 ). We will also freely use
standard Boolean connectives such as →, etc.
As a simple example, consider the following LKS M . It has two states, the leftmost of which (doubly
circled) is the sole initial state. Its set of atomic state propositions is {p, q, r}; the first state is labelled with{p, q} and the second with {q, r}. M ’s transitions are similarly labelled with sets of events drawn from thealphabet {a, b, c, d}.
4

By convention, an infinite sequence is prefix of another one iff they are the same.

8

Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha

a,b
c
q,r

p,q
d

As the reader may easily verify, M  G(c → Fr) but M 2 G(b → Fr). Note also that M  G(d → Fr) 5 ,but M 2 G(d → XFr).
We remark that SE-LTL formulas conform with our intuitive interpretation of specifications provided
that the LKSs under consideration are deadlock-free: indeed, an LKS with no infinite path, for example,
vacuously satisfies any SE-LTL formula! Deadlock checking is therefore a vital prerequisite for ensuring
the soundness of our analysis. A system found to exhibit deadlock should be sent back to its designer for
debugging; if it turns out the deadlocks somehow do not correspond to genuine bugs, then at the very least
they should be managed via the ‘soft’ sink-state-based approach discussed in Section 3.
Let us record the following proposition, which validates our decision not to distinguish between ∼equivalent LKSs:
Proposition 3. Let M and M 0 be LKSs with M ∼ M 0 . Then, for any SE-LTL formula φ, M  φ iff M 0  φ0 .

4.1. Automata-based Verification
We aim to reduce SE-LTL verification problems to standard automata-theoretic techniques for LTL. Notethat a straightforward—but unsatisfactory—way of achieving this is to explicitly encode actions throughchanges in (additional) state variables, and then proceed with LTL verification. Unfortunately, this trick
usually leads to a significant blow-up in the state space, and consequently yields much larger verification
times. The approach we present here, on the other hand, does not alter the size of the LKS, and is therefore
considerably more efficient.
We first recall some basic results about LTL, Kripke structures, and automata-based verification.
A Kripke structure is simply an LKS minus the alphabet and the transition-labelling function. An LTL
formula is an SE-LTL formula that makes no use of events as atomic propositions.
P
For P a set of atomic propositions, let BP ∼= 22 denote the set of Boolean combinations of atomic
propositions in P .
A Büchi automaton is a 6-tuple B = (SB , Init B , P, LB , TB , Acc) with SB a finite set of states, Init B ⊆ SBa set of initial states, P a finite set of atomic state propositions, LB : SB → BP a state-labelling function,
T ⊆ SB × SB a transition relation, and Acc ⊆ SB a set of accepting states.
Note that the transition relation is unlabelled, and that the states of a Büchi automaton are labelledwith arbitrary Boolean combinations of atomic propositions.
For π an infinite sequence of states of a Büchi automaton, let inf(π) ⊆ SB be the set of states which
occur infinitely often in π. π is accepted by the Büchi automaton B if it is Init B -rooted, if it is consistent
with the transition relation, and if inf(π) ∩ Acc 6= ∅. The set of all such accepted paths is written Path(B).
Let M = (S, Init, P, L, T ) be a Kripke structure. The state-labelling function L : S → 2 P indicates, foreach state s ∈ S, exactly which
atomicV
V propositions hold at s; such labelling is equivalent to asserting thatthe compound proposition L(s) ∧ {¬p | p ∈ P \ L(s)} holds at s. Let us denote this compound proposition
g Every Kripke structure can therefore be viewed as a Büchi automaton, where we consider everyby L(s).
state to be accepting.
Let B = (SB , Init B , P, LB , TB , Acc) be a Büchi automaton over the same set of atomic propositions as
M . We can define the ‘standard’ product M × B = (S 0 , Init 0 , −, −, T 0 , Acc 0 ) as a product of Büchi automata.
More precisely,
5

Indeed, according to the semantics, a path satisfies the formula d iff d is the first event following the initial state of the path.
Observe now that the only state from which d is immediately possible if the right-hand one, in which r holds, and therefore inwhich a fortiori Fr holds. This example highlights a somewhat counterintuitive feature of our semantics in which states andevents are combined.

Concurrent Software Verification with States, Events, and Deadlocks

9

g implies LB (b)},1. S 0 = {(s, b) ∈ S × SB | L(s)0 0
2. (s, b) −→ (s , b ) iff s −→ s0 and b −→ b0 ,3. (s, b) ∈ Init 0 iff s ∈ Init and b ∈ Init B , and4. (s, b) ∈ Acc 0 iff b ∈ Acc.
The non-symmetrical standard product M × B accepts exactly those paths of M which are ‘consistent’with B. Its main technical use lies in the following result of Gerth et al. [GPVW95]:
Theorem 2. Given a Kripke structure M and LTL formula φ, there is a Büchi automaton B ¬φ such thatM  φ iff Path(M × B¬φ ) = ∅.
An efficient tool to convert LTL formulas into optimized Büchi automata with the above property is
Somenzi and Bloem’s Wring [WRING, SB00].
We now turn to labelled Kripke structures. Let M = (S, Init, P, L, T, Σ, E) be an LKS. Recall that SELTL formulas allow events in Σ to stand for atomic
propositions. For x ∈ Σ, let us therefore write xe toVdenote the (formal) compound proposition x ∧ {¬y | y ∈ Σ \ {x}}. We can also, given an SE-LTL formula
φ over P and Σ, interpret φ as an LTL formula over P ∪ Σ (viewed as atomic state propositions); let us
denote the latter formula by φ[ . φ[ is therefore syntactically identical to φ, but differs from φ in its semanticinterpretation.
We now define the state/event product of a labelled Kripke structure with a Büchi automaton. Let M
be as above, and let B = (SB , Init B , P ∪ Σ, LB , TB , Acc) be a Büchi automaton over the set of atomic state
propositions P ∪ Σ. The state/event product M ⊗ B = (S 0 , Init 0 , −, −, T 0 , Acc 0 ) is a Büchi automaton thatsatisfies
g implies ∃Σ  LB (b)},6
1. S 0 = {(s, b) ∈ S × SB | L(s)xg ∧x
2. (s, b) −→ (s0 , b0 ) iff there exists x ∈ Σ such that s −→ s0 and b −→ b0 and (L(s)e) implies LB (b),03. (s, b) ∈ Init iff s ∈ Init and b ∈ Init B , and4. (s, b) ∈ Acc 0 iff b ∈ Acc.
Finally, we have:

Theorem 3. For any LKS M and SE-LTL formula φ,
M  φ iff Path(M ⊗ B¬φ[ ) = ∅.
Note that the state/event product does not require an enlargement of the LKS M (although we consider
below just such an enlargement in the course of the proof of the theorem).
Proof. Observe that a state of M can have several differently-labelled outgoing transitions. However, byduplicating states (and transitions) as necessary, we can transform M into a ∼-equivalent LKS M 0 having
the following property: for every state s of M 0 , the transitions emanating from s are all labelled with thesame (single) event. As a result, the validity of an SE-LTL atomic event proposition a in a given state ofM 0 does not depend on the particular path to be taken from that state, and can therefore be recorded as apropositional state variable of the state itself. Formally, this gives rise to a Kripke structure M 00 over atomic
state propositions P ∪ Σ.
We now claim that
Path(M ⊗ B¬φ[ ) = ∅ iff Path(M 00 × B¬φ[ ) = ∅.

(1)00

To see this, notice first that there is a bijection between Path(M ) and Path(M ) (which we denote π 7→ π 00 ).
Next, observe that any path in Path(M ⊗ B¬φ[ ) can be decomposed as a pair (π, β), where π ∈ Path(M )and β ∈ Path(B¬φ[ ); likewise, any path in Path(M 00 × B¬φ[ ) can be decomposed as a pair (π 00 , β), where
π 00 ∈ Path(M 00 ) and β ∈ Path(B¬φ[ ). A straightforward inspection of the relevant definitions then reveals
that (π, β) ∈ Path(M ⊗ B¬φ[ ) iff (π 00 , β) ∈ Path(M 00 × B¬φ[ ), which establishes our claim.
Finally, we clearly have M  φ iff M 0  φ iff M 00  φ[ . Combining this with Theorem 2 and Equation 1
above, we get M  φ iff Path(M ⊗ B¬φ[ ) = ∅, as required.
6 The term ∃Σ  L (b) denotes the formula L (b) in which all atomic Σ-propositions have been existentially quantified out; inB
B
practice, however, the output of Wring is presented in a format for which this operation is trivial.

10

Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha

m2
m1 c0 c1
m0
c0

m1
m=0

m2
m=1

m0

m=2
m1

m2
c0
c1
c2

m0
Fig. 1. The LKS of a surge protector.

The significance of Theorem 3 is that it enables us to make use of the highly optimized algorithms andtools available for verifying LTL formulas on Kripke structures to verify SE-LTL specifications on labelled
Kripke structures, at no additional space or time costs (no change in the sizes of the LKS M or the formulaφ).
Note that a Büchi automaton has non-empty accepted language iff it accepts a lasso, i.e., a path consistingof a finite prefix leading to an infinite loop. Efficient algorithms for checking emptiness of Büchi automata
are well-known, see e.g., [CGP99]. Moreover, these algorithms can always be required to produce an explicit
witness in the case of non-emptiness. Since a lasso in M ⊗ B¬φ[ clearly projects onto a lasso in M , we havethe following:
Theorem 4. For an LKS M and an SE-LTL formula φ, if M 2 φ, then one can extract a lasso π ∈ Path(M )such that π 2 φ.
Such counterexamples allow us to incrementally refine our abstractions during model checking.

5. A Surge Protector
We describe a toy model of a safety-critical current surge protector in order to illustrate the advantages ofstate/event-based implementations and specifications over both the pure state-based and the pure eventbased approaches.
The surge protector is meant at all times to disallow changes in current beyond a varying threshold. The
labelled Kripke structure in Figure 1 captures the main functional aspects of such a protector in which thepossible values of the current and threshold are 0, 1, and 2. The threshold value is stored in the variable m,
and changes in threshold and current are respectively communicated via the events m0, m1, m2, and c0, c1,
c2.7 Note, for instance, that when m = 1 the protector accepts changes in current to values 0 and 1, but not
2 (in practice, an attempt to hike the current up to 2 should trigger, say, a fuse and a jump to an emergency
state, behaviours which are here omitted for simplicity).
The required specification is neatly captured as the following SE-LTL formula:φse = G((c2 → m = 2) ∧ (c1 → (m = 1 ∨ m = 2))).
By way of comparison, Figure 2 represents the (event-free) Kripke structure that captures essentiallythe same behaviour as the LKS of Figure 1. In this pure state-based formalism, nine states are required tocapture all the reachable combinations of threshold (m = i) and last current changes (c = j) values.
The data (9 states and 39 transitions) compares unfavourably with that of the LKS in Figure 1 (3 states
and 9 transitions). Moreover, as the allowable current ranges increase, the number of states of the LKS willgrow linearly, as opposed to quadratically for the Kripke structure. The number of transitions of both willgrow quadratically, but with a roughly four-fold larger factor for the Kripke structure. These observations
7 The reader may object that we have only allowed for Boolean variables in our definition of labelled Kripke structures; itis however trivial to implement more complex types, such as bounded integers, as Boolean encodings, and we have therefore
elided such details here.

Concurrent Software Verification with States, Events, and Deadlocks

11

m=0
c=0

m=1
c=0

m=2
c=0

m=0
c=1

m=1
c=1

m=2
c=1

m=0
c=2

m=1
c=2

m=2
c=2

Fig. 2. The Kripke structure of a surge protector.

highlight the advantages of a state/event approach, which of course will be more or less pronounced dependingon the type of system under consideration.
Another advantage of the state/event approach is witnessed when one tries to write down specifications.
In this instance, the specification we require is
φs = G(((c = 0 ∨ c = 2) ∧ X(c = 1)) → (m = 1 ∨ m = 2))∧G(((c = 0 ∨ c = 1) ∧ X(c = 2)) → m = 2),
which is arguably significantly more complex than φse .
The pure event-based specification φe capturing the same requirement is also clearly more complex thanφse :φe = G(m0 → ((¬c1) W (m1 ∨ m2)))∧G(m0 → ((¬c2) W m2))∧
G(m1 → ((¬c2) W m2)).
The greater simplicity of the implementation and specification associated with the state/event formalism
is not purely a matter of aesthetics, or even a safeguard against subtle mistakes; experiments also suggestthat the state/event formulation yields significant gains in both time and memory during verification. We
implemented three parameterized instances of the surge protector as simple C programs, in one case allowing
message passing (representing the LKS), and in the other relying solely on local variables (representing the
Kripke structure). We also wrote corresponding specifications respectively as SE-LTL and LTL formulas(as above) and converted these into Büchi automata using the tool Wring [WRING]. Figure 3 records thenumber of Büchi states and transitions associated with the specification, as well as the time taken by magic
to construct the Büchi automaton and confirm that the corresponding implementation indeed meets the
specification. The parameter Range indicates the maximum allowable current value.
A careful inspection of the table in Figure 3 reveals several consistent trends. First, the number of Büchistates increases quadratically with the value of Range for both the pure state-based and pure event-basedformalisms. In contrast, the increase is only linear when both states and events are used. We notice a similar
pattern among the number of transitions in the Büchi automata. The rapid increase in the sizes of Büchi
automata will naturally contribute to increased model checking time. However, we notice that the major
portion of the total verification time is required to construct the Büchi automaton. While this time increases
rapidly in all three formalisms, the growth is observed to be most benign for the state/event scenario. The

12

Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha
&

'

)
(
+
*

0

1
,., ,,/&,.)


 

  "!#$!#  % !#"!#   "!#
$!#' ( &())*) + ,.- &'()&- ) ' ,.*'&(&* ,/& &0('( ,/& &) (++0' ' + &1*'-0,' &) '1& ,,'2, &- '2, ,/(10 ,00- ( * &'))1 ,&& )* ,.-(+ &)&+ )- +' )01( '2,.-' + ,.- )-+'10)& (0 &'&* '* ,.* '& 1& ,/&-00 ,/&++- 0 ,/& + ,'1+&'' *- +&'1 ,.-)(* (+ ,/&( ('&-* ((-+' * ,' 1)- ,.)&,(* ,.-0 ,0(-) &'+-) 0& ,.+) )0&0*' )0'2,.++ 1 ,.+ &+&& ) ,.))0' ,.)* ((1(- +0(() 3 3
33,.- ,.* *0(- 1'**1& ,0) ,.1(04,.* &,.)1+1 3 3
33,, &- ))((+ )'(-)
3 3
3
3
3 3
3
3
,/& && ,.)(&(& ,.)+(-3 3
3
3
3 3
3
3
,.) &' ()'1 ,' ()+'(,
3 3
3
3
3 3
3
3
3 3
3
3

Fig. 3. Comparison of pure state-based, pure event-based and state/event-based formalisms. Values of c and m range between
0 and Range. St and Tr respectively denote the number of states and transitions of the Büchi automaton corresponding to
the specification. B-T is the Büchi automaton construction time and T-T is the total verification time. All times are reported
in milliseconds. A ∗ indicates that the verification did not terminate in 10 minutes.

net result is clearly evident from Figure 3. Using both states and events allows us to push the limits of c andm beyond what is possible by using either states or events alone.

6. Compositional Counterexample-guided SE-LTL Verification
We now discuss how our framework enables us to verify SE-LTL specifications on parallel compositions oflabelled Kripke structures incrementally and compositionally.
When trying to determine whether an SE-LTL specification holds on a given LKS, the following result
is the key ingredient needed to exploit abstractions in the verification process:
Theorem 5. Let M and A be LKSs with M v A. Then for any SE-LTL formula φ over M which mentions
only propositions (and events) of A,
if A  φ then M  φ.
Proof. This follows easily from the fact that every path of M is matched by a corresponding propertypreserving path of A.
Suppose now that we are given a collection M1 , . . . , Mn of LKSs, as well as an SE-LTL specification φ,with the task of determining whether M1 k . . . k Mn  φ. Let us assume that M1 k . . . k Mn is deadlockfree, a requirement for which we provide an algorithm in Section 9.8 We first create initial abstractions
A1 w M1 , . . . , An w Mn , in a manner to be discussed shortly. We then check whether A1 k . . . k An  φ. In
the affirmative, we conclude (by Theorems 1 and 5) that M1 k . . . k Mn  φ as well. In the negative, we areprovided (thanks to Theorem 4) with an abstract counterexample π ∈ Path(A 1 k . . . k An ) such that π 2 φ.
We must then determine whether this counterexample is real or spurious, i.e., whether it corresponds to a
counterexample in M1 k . . . k Mn or not.
This validation check can be performed compositionally, as follows. According to Theorem 1, the counterexample is real iff for each i, the projection πAi corresponds to (the prefix of) a valid behaviour of Mi .
To this end, we ‘simulate’ πAi on Mi . If Mi accepts the path, we go on to the next component. Otherwise,
we refine our abstraction Ai , yielding a new abstraction A0i with Mi v A0i v Ai and such that A0i also rejects
the projection πA0i of the spurious counterexample π. Note that if π is a lasso (as per Theorem 4), theprojection πAi is either a lasso or a finite path.
8 Of course, as explained in Section 4, the procedure given here will work perfectly well whether or not M k . . . k M isn1deadlock-free. Unfortunately, for deadlocking systems, the answer we get may not conform with our intuitive understanding of
the specification φ. For that reason, an initial deadlock-freedom check is highly recommended.

Concurrent Software Verification with States, Events, and Deadlocks

13

Algorithm SE-LTL Model Checking (M1 , . . . , Mn ; φ)for i := 1 to n : let ≈i := the coarsest partition of Mi that respects the atomic state propositions in φ;repeat foreverdecide whether M1 /≈1 k . . . k Mn /≈n  φ via automata-based algorithm (Theorems 3 and 4);
if there is no counterexample thenreturn “M1 k . . . k Mn  φ”else suppose π ∈ Path(M1 /≈1 k . . . k Mn /≈n ) violates φ;find i such that SE -LTL Validate/Refine(Mi , ≈i , πMi /≈i ) reports “spurious”;
if no such i thenreturn “M1 k . . . k Mn 2 φ ” along with counterexample derived from πelse refine ≈i to rule out spurious counterexample πMi /≈i ;endrepeat
Fig. 4. The overall SE-LTL model checking algorithm for a concurrent system M 1 k . . . k Mn and specification φ.

This process is iterated until either the specification is proved, or a real counterexample is found. Termination follows from the fact that the LKSs involved are all finite, and therefore admit only finitely many
distinct abstractions.9
The advantage of this approach is that the abstractions that we consider here, as detailed in Section 3,
are obtained by lumping together states of the original LKSs, and have therefore smaller state spaces. Sincecomposing components in parallel can in general lead to an exponential blow-up of the state space, theoverall reduction in size obtained by composing the reduced abstractions together can be enormous.
Let us return to our SE-LTL specification φ, and let us fix throughout Pφ to be the set of all atomic
state propositions appearing in φ. Consider any of the Mi ’s. Recall from Section 3 that an abstraction of
Mi is entirely determined by a Pφ -respecting partition ≈i of the set of states of Mi : such an abstraction isdenoted Mi /≈i .
The initial abstraction Mi /≈1i is the coarsest possible: s ≈1i s0 iff Li (s) ∩ Pφ = Li (s0 ) ∩ Pφ . Suppose now
that we are handed πi ∈ Path(Mi /≈ki ) ∪ FPath(Mi /≈ki ) (i.e., πi is either a lasso or a finite path of Mi /≈ki ).
We must determine whether πi is a real or spurious counterexample component, i.e., whether πi gives rise
to a valid path of Mi or not. Moreover, in the latter case, we want to refine our partition ≈ki into ≈k+1
soi
k+1
that πi is rejected by Mi /≈i .
This validation/refinement step proceeds as follows. For any set Q of states of M i and event a, letaSucc(Q, a) = {s0 | ∃s ∈ Q  s −→ s0 } denote the set of a-successors of Q in Mi . Let us first suppose that
πi = hs1 , a1 , s2 , a2 , . . . , am , sm+1 i is a finite path of Mi /≈ki . Start with the set Q1 = Init i ∩ s1 of those initialstates of Mi that belong to s1 , and compute successively Qj+1 = Succ(Qj , aj ) ∩ sj+1 . If, upon reaching
the end of πi , Qm+1 is non-empty, then clearly πi is a valid finite path of Mi . Otherwise, let Qj+1 be thefirst empty set thus generated. Refine the partition ≈ki by splitting sj into Qj and sj \ Qj , yielding a newpartition ≈k+1
. It is then easy to see that Mi /≈k+1
will reject πi .
ii
In case πi is a lasso, things are slightly more complicated. If Mi rejects πi , then the algorithm above will
establish this in the very same manner, by eventually producing an empty set of states Q j+1 . On the other
hand, if πi is accepted by Mi then there will be sets of states Qj = Qj+p such that Qj+p is obtained from
Qj by following the loop part of πi a finite number of times. Since all state spaces involved are finite thesearch will always terminate with one or the other answer after a finite number of iterations.
This validation/refinement step is similar to that originally proposed by Clarke et al. [CGJ + 00]; seealso [COYC03]. Let us refer to this procedure as SE -LTL Validate/Refine(M i , ≈i , πi ). The full algorithm forchecking whether M1 || . . . ||Mn  φ is given in Figure 4. Note that the abstraction, counterexample-validation,and refinement steps are all performed one component at a time.

9

When the LKSs M1 , . . . , Mn are generated from C programs via predicate abstraction, as is the case for magic, termination
will depend on whether magic is eventually able to generate sufficiently strong predicates. Although this in general cannot
be guaranteed, as a result of the undecidability of the halting problem, in practice it has not been observed to cause majordifficulties.

14

Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha

a

q

b
s

p
a

b
r

M1

c

t

w

a

x

b’

y

c

z

M2

Fig. 5. Two sample LTSs M1 and M2 . Initial states are doubly circled.

7. Deadlock
As explained earlier, as a result of our blocking message-passing semantics, a parallel composition M 1 k . . . k
Mn of components may exhibit deadlock (reaching a state with no outgoing transition), even if each M i isdeadlock-free. Deadlock corresponds to inconsistent communication requirements among the M i ’s.
An important observation is that deadlock is exclusively a function of the communication structure of
LKSs, and does not depend in any way on local variables (atomic state propositions), since our framework
does not allow these to be shared. In other words, if a particular parallel composition of LKSs exhibits
deadlock, then the deadlock will remain regardless of any changes to the various state-labelling functions of
its components, and likewise for deadlock-free systems. For this reason, we shall work in the remainder ofthis paper with labelled transition systems (LTS s for short) rather than LKSs.
An LTS is simply an LKS minus the state proposition structure: in other words a quintuple (S, Init, T, Σ, E)
with the same conventions as for LKSs. Given such an LTS M we occasionally write S(M ) and Σ(M ) todenote S and Σ respectively.
Paths are defined in the same manner as for LKSs, except that from now on we are exclusively concernedwith the finite variety. Recall that FPath(M ) stands for the set of finite paths accepted by the LTS M . A
trace over some alphabet Σ is a finite sequence of events of Σ. A trace ha 1 , a2 , . . . , am i over Σ(M ) is acceptedby M iff there exist s1 , s2 , . . . , sm+1 such that hs1 , a1 , s2 , a2 , . . . , am , sm+1 i ∈ FPath(M ). Paths and traces
are usually represented with the letters π and θ respectively.
A state s ∈ S(M ) is said to refuse an event a ∈ Σ(M ) iff there is no transition from s labelled by a. Thearefusal of a state s is the set of all events that it refuses: Ref (s) = {a ∈ Σ(M ) | @s 0 ∈ S(M )  s −→ s0 }.
Let θ be a trace of M and let F ⊆ Σ(M ) be a set of events. Suppose that M can accept θ along some
path ending in a state s with Ref (s) = F . Then we say that (θ, F ) is a failure of M . We write Fail (M ) todenote the set of all failures of M . Note that several failures can share the same trace component, since agiven trace may be accepted along more than one path.
Let M1 and M2 be two LTSs over a common alphabet Σ(M1 ) = Σ(M2 ). We say that M1 and M2 are
failure-equivalent if Fail (M1 ) = Fail (M2 ).
Finally, we say that M has a deadlock if it can reach a state which refuses its entire alphabet Σ(M ), inother words if (θ, Σ(M )) ∈ Fail (M ) for some θ.
Notice that two failure-equivalent LTSs will have identical deadlocking behaviour (or lack thereof). Since
failure-equivalence is preserved by parallel composition (see Theorem 6 below), we shall only be interested
in LTSs up to failure-equivalence.
The notions of refusal, failure, and deadlock that we are using here are borrowed from CSP (with minor
modifications10 )—see [Hoa85, Ros97].
As a simple example, consider the LTSs M1 and M2 depicted in Figure 5. Let Σ(M1 ) = {a, b, c} andΣ(M2 ) = {a, b0 , c}. Then M1 has seven paths: hpi, hp, a, qi, hp, a, ri, hp, a, q, b, si, hp, a, r, b, si, hp, a, q, b, s, c, ti,
and hp, a, r, b, s, c, ti. It has four traces: hi, hai, ha, bi, and ha, b, ci, and four failures (hi, {b, c}), (hai, {a, c}),(ha, bi, {a, b}), and (ha, b, ci, {a, b, c}). Hence M1 has a deadlock. Also, M2 has four paths, four traces, four
failures and a deadlock.
The notion of projection defined in Section 3 carries over naturally to traces. Let M be an LTS, and let

10 The main difference is that our refusals are maximal, whereas in the CSP semantics refusals are only required to be subsets
of disabled events. This distinction is immaterial insofar as deadlock-checking is concerned.

Concurrent Software Verification with States, Events, and Deadlocks

b’

q,y
b

q,x
a

15

b

p,w

s,x

b’

s,y

c

t,z

b

a
r,x

b
b’

r,y

Fig. 6. Parallel composition of LTSs M1 and M2 from Figure 5.

θ be a sequence of events, which may or may not belong to Σ(M ). The projection θM of θ on M consistsof the subsequence of θ obtained by simply removing all events not belonging to Σ(M ).
Recall the notion of parallel composition from Section 3. Figure 6, for example, shows the LTS M 1 k M2
where M1 and M2 are the LTSs shown in Figure 5. Note that its alphabet is {a, b, c} ∪ {a, b0 , c} = {a, b, b0 , c}.
The following Theorem lists well-known results from CSP [Ros97].
Theorem 6.
1. Parallel composition is associative and commutative up to failure-equivalence. Thus, in particular, nobracketing is required when combining more than two LTSs.
2. Parallel composition is a congruence with respect to failure-equivalence: let M 1 , M10 , M2 , M20 , . . . , Mn , Mn0
be LTSs, with each Mi failure-equivalent to Mi0 . Then M1 k . . . k Mn is failure-equivalent to M10 k . . . k
Mn0 .
3. Let M1 , . . . , Mn be LTSs, θ a sequence of events, and F aSset of events. Then (θ, F ) ∈ Fail (M1 k . . . k Mn )niff there exist sets of events F1 , . . . , Fn such that (i) F = i=1 Fi , and (ii) for each i, (θMi , Fi ) ∈ Fail (Mi ).
In other words, whether a parallel composition of LTSs has a given failure can be checked by projecting
and examining the failure on each individual component separately.
Theorem 6(3) highlights the compositional aspect of failures and is a key ingredient of our deadlockdetection algorithm, which we present in Section 9.

8. Abstraction
In this section we introduce the abstractions that we shall use in the remainder of this paper. Once again
these abstractions are based on existential quotients of LTSs (see Section 3), although as we shall see quotient
LTSs on their own are inadequate for deadlock detection.
Recall that quotient LTSs are obtained by lumping together states of a given LTS. Since there are no
atomic state propositions to respect in the case of LTSs, any partition of the state space of an LTS gives
rise to a bona fide quotient LTS. For M an LTS and ≈ a partition of S(M ), we again write M/≈ to denote
the resulting quotient LTS. The states of M are said to be concrete states, and are usually represented
with lowercase Roman letters such as s, whereas the states of M/≈, which are called abstract states, arerepresented either as equivalence classes (e.g., [s]) or with the lowercase Greek letter α.
The existential nature of the transition relation of quotient LTSs immediately yields the following:
Proposition 4. Let M be an LTS and M/≈ a quotient LTS of M . For any path hs1 , a1 , s2 , . . . , am , sm+1 i ∈FPath(M ), we have h[s1 ], a1 , [s2 ], a2 , . . . , am , [sm+1 ]i ∈ FPath(M/≈).
Note the following facts about the LTSs in Figure 7: (i) M1 and M2 both have deadlocks but M1 k M2
does not; (ii) neither M3 nor M4 has a deadlock but M3 k M4 does; (iii) M1 has a deadlock and M3 does nothave a deadlock but M1 k M3 has a deadlock; (iv) M1 has a deadlock and M4 does not have a deadlock but
M1 k M4 does not have a deadlock (assuming that Σ(M4 ) = {a, b}); (v) M1 has a deadlock but the quotient

16

Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha

c

a

b

b

c

a
M2

M1

a
M3

b

b
M4

a

a

p b

q

c

r

M5

Fig. 7. Five sample LTSs. Initial states are doubly circled.

LTS obtained by lumping all the states of M1 into a single equivalence class does not have a deadlock;(vi) finally, M5 has no deadlock (since state r cannot be reached from the initial state p), yet the quotient
LTS obtained by lumping together states p and q does have a deadlock.
These examples highlight the following facts: (i) deadlock is inherently non-compositional: neither its
presence nor its absence is preserved by parallel composition; (ii) existential abstractions on their own
are inadequate for handling deadlock: they preserve neither its presence nor its absence. (We remark that
universal abstractions are likewise inadequate for handling deadlock, for the same reason.)
The inadequacy of existential abstractions with respect to deadlock is to be contrasted with their adequacy
for SE-LTL: existential quotients preserve the non-satisfaction of SE-LTL formulas (as per Theorem 5), andthus lead to an iterative algorithm for model checking SE-LTL formulas. In order to be able to do the samefor deadlock detection, we need to equip our existential abstractions with additional structure.
Let us take a closer look at the non-preservation of deadlock by existential
abstractions. Consider aTquotient LTS M/≈ and a state α of M/≈. It is easy to see that Ref (α) = s∈α Ref (s). In other words, therefusal of an abstract state α under-approximates the refusals of each of its corresponding concrete states.
In order to preserve deadlock, we must instead require that refusals of concrete states be over-approximated.
This can be achieved by simply taking the union of the refusals of the concrete states. This leads us to thenotion of abstract refusals, which we now define formally.
Let M be an LTS and ≈ a partition of the state space of M . For any abstract state α ∈ S(M/≈), define
the abstract refusal of α to be[
AbsRef (α) =Ref (s).
s∈αMoreover, for a parallel composition M1 /≈1 k . . . k Mn /≈n of quotient LTSs, we extend the notion of
abstract refusal by letting, for any α = (α1 , . . . , αn ) ∈ S(M1 /≈1 k . . . k Mn /≈n ),AbsRef (α) =n[AbsRef (αi ).

i=1This naturally leads us to the notion of abstract failures, which are similar to failures, except that refusals
c be an LTS for which abstract refusals are defined (i.e., M
c is either aare replaced by abstract refusals. Let M
ccquotient LTS or a parallel composition of such). Let θ be a trace of M and let F ⊆ Σ(M ) be a set of events.
c can accept θ along some path ending in a state α with AbsRef (α) = F . Then we say that
Suppose that M
c. We write AbsFail (Mc) to denote the set of all abstract failures of Mc.
(θ, F ) is an abstract failure of M
The following lemma essentially states that the failures of an LTS M are always subsumed by the abstract
failures of its quotient LTS M/≈:
Lemma 1. Let M be an LTS, ≈ a partition of the state space of M , and M/≈ the quotient LTS inducedby ≈. Then for all (θ, F ) ∈ Fail (M ), there exists F 0 ⊇ F such that (θ, F 0 ) ∈ AbsFail (M/≈).
Proof. This is a straightforward consequence of Proposition 4.
The following lemma shows that abstract failures, like failures, are compositional: the abstract failuresof a concurrent system Mk can be decomposed naturally into abstract failures of each of its components.
Lemma 2. Let M1 /≈1 , . . . , Mn /≈n be quotient LTSs, θ a sequence of events, and F a set of events.
SnThen(θ, F ) ∈ AbsFail (M1 /≈1 k . . . k Mn /≈n ) iff there exist sets of events F1 , . . . , Fn such that (i) F = i=1 Fi ,and (ii) for each i, (θMi /≈i , Fi ) ∈ AbsFail (Mi /≈i ).
Proof. This follows from the fact that θ is a trace of M1 /≈1 k . . . k Mn /≈n iff for each i, θMi /≈i is a traceof Mi /≈i , which itself is implied by Theorem 6(3).

Concurrent Software Verification with States, Events, and Deadlocks

17

the paper we shall often use the following facts implicitly: Σ(M 1 /≈1 k . . . k Mn /≈n ) =Sn In the remainderSofni=1 Σ(Mi /≈i ) =i=1 Σ(Mi ) = Σ(M1 k · · · k Mn ).
ck = M1 /≈1 k . . . k Mn /≈n
Abstract failures lead naturally to the notion of abstract deadlocks. Let Mcck )) ∈
be a parallel composition of quotient LTSs. Then Mk is said to have an abstract deadlock if (θ, Σ(Mck ) for some trace θ of M
ck . In other words, abstract deadlocks arise from traces in the abstracted
AbsFail (Msystem that lead to an abstract refusal of the entire alphabet.

9. Compositional Counterexample-guided Deadlock Detection
We now discuss how the abstractions defined in the previous section enable us to decide incrementally andcompositionally whether or not a parallel composition of LTSs is deadlock-free.
Analogously to Theorem 5, the following result is the key ingredient needed to exploit our abstractionsin the deadlock-checking process:
Theorem 7. Let M1 , . . . , Mn be LTSs, and let ≈1 , . . . , ≈n be partitions of the state spaces of the Mi
respectively. If M1 /≈1 k . . . k Mn /≈n has no abstract deadlock, then M1 k . . . k Mn is deadlock-free.
ck = M1 /≈1 k
Proof. Let us establish the contrapositive. To this end, write Mk = M1 k . . . k Mn and M. . . k Mn /≈n , and suppose that (θ, Σ(Mk )) ∈ Fail (Mk ). By Theorem 6(3), there are sets of events F1 , . . . , Fn
whose union is Σ(Mk ) and such that (θMi , Fi ) ∈ Fail (Mi ) for each i. From Lemma 1, there are sets of events
F10 , . . . , Fn0 with each Fi0 ⊇ Fi and such that (θMi , Fi0 ) ∈ AbsFail (Mi /≈i ) for each i. Since θMi = θMi /≈i ,ck )) ∈ Fail (Mck ).
we can invoke Lemma 2 to conclude that (θ, Σ(Mck has an abstract deadlock iff it has a finite path that reaches a state whose abstract refusal
Note that M
ck ). We call such a path a counterexample to abstract deadlock-freedom, or simply anis the whole of Σ(Mabstract counterexample. One must then determine whether this abstract counterexample is valid or not,i.e., whether it gives rise to a genuine deadlock in the concrete system or not.
Suppose that our abstract counterexample is π = hα1 , a1 , α2 , a2 , . . . , am , αm+1 i, where we write αm+1 =
1
n
(αm+1
, . . . , αm+1). Let θ = ha1 , a2 , . . . , am i be the trace associated with π. Then for each i, we have thati(θMi /≈i , AbsRef (αm+1)) is an abstract failure of Mi /≈i . If it turns out also to be a genuine failure of
Mi , for each Mi , then we say that the abstract counterexample is valid. Indeed we can conclude, thanks to
Theorem 6(3), that Mk has a genuine deadlock, which moreover we can readily provide a witness for.
Efficient algorithms for checking whether an LTS has a given failure are well-known—see, e.g., [Ros97].
Note that the validation is performed compositionally, one component (M i ) at a time.
i
Unfortunately, we may instead discover some Mi for which (θMi , AbsRef (αm+1)) is not a failure. In thatcase, we must refine our partition ≈i , so as to rule out the spurious abstract failure, and start the searchanew. Note once again that termination will follow automatically provided that each partition refinement isstrict.11
The refinement step proceeds as follows. We are assuming that either (i) the path π i = hα1i , a1 , α2i , a2 , . . . ,iam , αm+1
i of Mi /≈i cannot be matched by Mi , or (ii) that it can be matched but that none of the states s itileads to has Ref (s) = AbsRef (αm+1). In case (i), we employ exactly the same technique as that of Section 6
ito refine the partition ≈i by splitting one of the intermediate abstract states α1i , . . . , αmin two. In case (ii),iwe observe that the states in αm+1 that are reachable in Mi along πi cannot all have identical refusals. Picksome event a for which at least two states disagree, and split αm+1 into those states that refuse a and thosethat do not. This clearly gives rise to a strict refinement of the partition ≈ i , and moreover permanently rulesout the spurious abstract counterexample π.
Let us refer to this procedure as Deadlock Validate/Refine(Mi , ≈i , πi ). The full algorithm for checking whether M1 || . . . ||Mn has a deadlock is given in Figure 8. Note that the abstraction, counterexamplevalidation, and refinement steps are all performed one component at a time.
11 In fact, it turns out that the abstract LTSs converge to the bisimulation quotients of their concrete counterparts; however
in practice deadlock-freedom is often established or disproved well before the bisimulation quotient is achieved.

18

Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha

Algorithm Deadlock Detection (M1 , . . . , Mn )for i := 1 to n : let ≈i := the coarsest partition, with all states in the same equivalence class;repeat foreverfind abstract deadlock in M1 /≈1 k . . . k Mn /≈n ;if there is no abstract deadlock thenreturn “M1 k . . . k Mn is deadlock-free”
else suppose π ∈ FPath(M1 /≈1 k . . . k Mn /≈n ) leads to abstract deadlock;find i such that Deadlock Validate/Refine(Mi , ≈i , πMi /≈i ) reports “spurious”;
if no such i thenreturn “M1 k . . . k Mn has deadlock” along with counterexample derived from πelse refine ≈i to rule out spurious counterexample πMi /≈i ;endrepeat
Fig. 8. The overall deadlock-detection algorithm for a concurrent system M 1 k . . . k Mn .

10. Experimental Results
We implemented our algorithms within the magic tool. magic extracts finite LKS models from C programs
using predicate abstraction. These LKSs are then analyzed to check for satisfaction of an SE-LTL specificationor the presence of deadlock using the techniques presented in this article. Once a real counterexample π isfound at the level of the LKSs magic analyzes π and, if necessary, creates more refined models by inferring
new predicates12 . Our actual implementation is therefore a two-level CEGAR scheme. We elide details of theouter predicate abstraction-refinement loop as it is similar to some of our previous work [COYC03]. All our
experiments were performed on an AMD Athlon XP 1600+ machine with 900 MB RAM running RedHat
Linux 7.1.

10.1. SE-LTL Experiments
In order to validate our approach for SE-LTL model checking we experimented with two broad sets ofbenchmarks. The first set of these examples was based on OpenSSL-0.9.6c, an open-source implementation of
the SSL protocol. This is a popular protocol used for secure exchange of sensitive information over untrusted
networks. SSL involves an initial handshake between a client and a server that attempt to establish a securechannel between themselves. The target of our verification process was the implementation of this handshake,comprising about 350 lines of ANSI C code each for the server and the client.
From the official SSL specification [SSL] we derived a set of nine properties that every correct SSL implementation should satisfy. The first five properties are relevant only to the server, the next two apply only tothe client, and the last two properties refer to both a server and a client executing concurrently. For instance,
the first property states that whenever the server asks the client to terminate the handshake, it eventuallyeither gets a correct response from the client or exits with an error code. The second property expresses
the fact that whenever the server receives a handshake request from a client, it eventually acknowledges therequest or returns with an error code. The third property states that a server never exchanges encryption
keys with a client once the cipher scheme has been changed.
Each of these properties were then expressed in SE-LTL, once using only states and again using bothstates and events. Table 9 summarizes the results of our experiments with these benchmarks. The SSL
benchmarks have names of the form x-y-z where x denotes the type of the property and can be either srvr,
clnt or ssl, depending on whether the property refers respectively to only the server, only the client, orboth server and client. y denotes the property number while z denotes the specification style and can beeither ss (only states) or se (both states and events). We note that in each case the numbers for state/event
properties are considerably better than those for the corresponding pure-state properties.
The second set of our benchmarks was obtained from the source code of version 2.0 of Micro-C/OS. Thisis a popular, lightweight, real-time, multi-tasking operating system written in about 3000 lines of ANSI C.
12 This is akin to the splitting of abstract states described in the paper, carried out symbolically via the use of predicates on
the state space of the C program.

Concurrent Software Verification with States, Events, and Deadlocks

19              "!# $  &%'(   )+*+,-*.0/1.)+)2
3354637/
87/(9 9687/:463 /(;63<2 9$26=645=.
)*>, *+.>/1.")?
922-8$;54
8$=54 /(@/6/(; /(9$264 /(45;-AB2.
)+*+,-*. 8B.)+) /5/ 859 2 4$2'/
8$468 9/(969/ 8<2-A<4 9$2'/:=68.
)*>, *+."8B.")?
922-8$;54/(45; /BA<@64 A /(9/BA /(4$2C/(=.
)+*+,-*."9<.)+) 9 A /(264 35=5;63 /5/D2-A 8$;54 3$@ 26=59/ 9687/:9 A.
)*>, *+.9<.")?
922-8$;54
26;68 /BA<4 3$= /(45=5@ 8$=59'/(4.
)+*+,-*.2$.)+) /(; 2C/ 3$2526;@5=5; 8$45@6=54 A<95@68 9545952'/ 8$@E ;)*>, *+. 2$.")?
A/(22 95959
2'/:3 87/D2-3$9 9637/(9 853$46=5; 8<2'EF/)+*+,-*. 3B.)+) 853 27A
A$4637/;545= 26@5@'/(= ;5@$2 8 3$;5@6@5@ 954E 9)*>, *+."3B.")? 8$= 2-3 2 959/264 A /(@5@6=5@ 8$46853 8586A$;63 8<2'E 8
G1HJI6K.0/1.)>) /(; 2C/ 2 @5; A
A<459 8<252 @5@ /:8$963 8$;54 3$9 8537E @G1HFI K.>/1.")?
A/(296;5459
9 A<; /BA$863$= 3$@59/(@5;6@59 8587EF/
G1HJI6K. 8B.)>) 853 27A
A536AB2;5454 269635468 /(;$264 26;$26252 95@EF/
G1HFI K."8B.")?
/(@ 2 =
96;54/26= A /:3$96=$2 /(=5@ A /BA$85;54 87/5E 8)+)HF.>/1.")+)
853 27A 8$2-A<4546358$@ @ AB2 ;63535@63LL@63$=EM3)>)HN.0/1.)+?
8$= 2-3 /:96353$@545@$2 ;6353 9595=64/ 87/BA$87/:954 858$=5;645@59 /(;687E 2)+)HF."8B.")+)
853 27A 9 853$4 A<=$2 8 @595; ;5;5= 8$4
LL
9$26;E ;)>)HN. 8B.)+?
/(@ 2 = /B3$4/5/BA<4/ A-/(9 9$26;52'/ 2'/D26@6363$= 2'/(@635=5;5@ 968$=EOA
PRQTSRU .V PXW @
/(2
@ A$9
8$=63 9$2 =54 8$;/95@6@5=.
PRQYS#U .>/
@
/(2
@ A$9
/(4$2 9596;63 86A<4 A;59 36A.
PRQYS#U ."8
3
@
@ A$9
/:8$9 959-A$8 8$;595=;/B86A.
Fig. 9. Experimental results with OpenSSL and Micro-C/OS. These experiments did not make use of abstraction/refinement
and proceeded in a single iteration. St(B) and Tr(B) = respectively the number of states and transitions in the Büchi
automaton; St(Mdl) = number of states in the model; T(Mdl) = model construction time; T(BA) = Büchi construction
time; T(Ver) = model checking time; T(Total) = total verification time. All reported times are in milliseconds. Mem is thetotal memory requirement in MB. A * indicates that the model checking did not terminate within 2 hours and was aborted. Insuch cases, other measurements were made at the point of forced termination. A - indicates that the corresponding measurement
was not taken.

The OS uses a lock to ensure mutual exclusion for critical section code. Using SE-LTL we expressed two
properties of the OS: (i) the lock is acquired and released alternately starting with an acquire and (ii) every
time the lock is acquired it is eventually released. These properties were expressed using only events.
We found a bug in the OS that causes it to violate the first property. We informed the developers of the
OS about this bug and were told that it had been detected and fixed. The developers also kindly supplied
us with the latest source code for the OS, and we are currently attempting to find errors in it. The second
property was found to be valid. In Figure 9 these experiments are named UCOS-BUG and UCOS-2 respectively.
Next we fixed the bug and verified that the first property holds for the corrected OS. This experiment iscalled UCOS-1 in Figure 9.
Since our main goal in these experiments was to directly compare the state/event-based and pure-statebased approaches, we did not make use of any abstraction and refinement at the level of the LKSs and theverification therefore proceeded in a single iteration.

10.2. Deadlock Experiments
Our approach for deadlock detection was validated against a broad set of benchmarks consisting of both industrial and classical systems. Our results are summarized in Figure 10. The ABB benchmark was provided
to us by our industrial partner, ABB Corporation [ABB]. It implements part of an inter-process communication protocol (IPC-1.6) used to mediate communication in a multi-threaded robotics control automation
system developed by ABB. The implementation is required to satisfy various safety-critical properties, and20

Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha

Name
ABB
SSL
UCOSD-2
UCOSD-3
UCOSN-4
UCOSN-5
UCOSN-6
RW-4
RW-5
RW-6
RW-7
RW-8
RW-9
DPN-3
DPN-4
DPN-5
DPN-6
DPD-9
DPD-10 Plain


 



49405

 
    
"!#$&% (  $&%' ) $+*' $&,**( / 0$&%($+*"!#$&,('*2*0*2

*
25731
5851
*
39262

 
*
8369
54369

('  
*
*
*
1401
16277

 
*
11278
38268

I
*
1
5
*
1
1
*
4
4
4
*
*
*
2
2
2
*
1
1

T
*
44
24
*
18.1
253
*
6.48
35.1
257
*
*
*
.779
11.8
197
*
22.5
87.6

M
162
43.5
14.5
58.6
14.1
52.2
219.3
10.8
15.9
45.2
178
*
*
10.9
28.0
203
12.0
17.3


 
16
374
6144
8192
65536

' 
5120
24576

  '   "!.
5832

 1  ( ' 1/$+%IterDeadlockI1973 861
16
16
261
77
4930 1202125
3012500 3771875 44
67
54
132
60
261
66
518
72
1031
78
2056
84
182
27
1274
34
8918
41
62426 4813069 4644493 51

T
1446
31.9
14.5
221.8
8.1
80
813
4.40
7.33
12.6
25.3
60.5
132
.849
7.86
84.6
831
191
755

M
33.3
40.8
12.9
15
10.5
12.7
30.8
10.0
10.4
10.8
11.8
14.0
14.5
9.5
11.4
26.1
12.2
18.4

Fig. 10. Experimental results. SM = maximum # of states; SR = # of reachable states; I = # of iterations; T = time inseconds; M = memory in MB; time limit = 1500 sec; - indicates negligible value; * indicates out of time; notable figures arehighlighted.

in particular deadlock-freedom. The IPC protocol supports multiple modes of communication, including
synchronous point-to-point, broadcast, publish/subscribe, and asynchronous communication. Each of thesemodes is implemented in terms of messages passed between queues owned by different threads. The protocol
handles the creation and manipulation of message queues, synchronizing access to shared data using various
operating system primitives (e.g., semaphores), and cleaning up internal states when a communication fails
or times out.
We analyzed the portion of the IPC protocol that implements the primitives for synchronous communication (approx. 1500 LOC) among multiple threads. With this type of communication, a sender sends a
message to a receiver and blocks until an answer is received or it times out. A receiver asks for its next
message and blocks until a message is available or it times out. Whenever the receiver gets a synchronous
message, it is then expected to send a response to the sender. magic successfully verified the absence of
deadlock in this implementation.
The SSL benchmark represents a deadlock-free system (approx. 700 LOC) consisting of one OpenSSL
server and one OpenSSL client. The UCOSD-n benchmarks are derived from Micro-C/OS version 2.7, areal-time operating system for embedded processors, and consist of n threads (approx. 6000 LOC) executing
concurrently. Access to shared data is protected via locks. This implementation suffers from deadlock. In
contrast, the UCOSN-n benchmarks are deadlock-free. The RW-n benchmarks implement a deadlock-freereader-writer system (194 LOC) with n readers, n writers, and a controller. The controller ensures that at
most one writer has access to the critical section. Finally, the DPN-n benchmarks represent a deadlock-free
implementation of n dining philosophers (251 LOC), while DPD-n implements n dining philosophers (163
LOC) that can deadlock. As Figure 10 shows, even though the implementations are of moderate size, thetotal state space is often quite large due to exponential blowup.
Values under IterDeadlock refer to measurements for our approach while those under Plain correspondto a naive approach involving only predicate abstraction refinement. We note that IterDeadlock outperforms
Plain in almost all cases. In many cases IterDeadlock is able to establish deadlock or deadlock-freedom while

Concurrent Software Verification with States, Events, and Deadlocks

21

Plain runs out of time. Even when both approaches succeed, IterDeadlock can yield over 20 times speed-up intime and require over 4 times less memory (RW-6 ). For the experiments involving dining philosophers withdeadlock however, Plain performs better than IterDeadlock. This is because in these cases Plain terminates
as soon as it discovers a deadlocking scenario, without having to explore the entire state space. In contrast,
IterDeadlock has to perform many iterations before finding a genuine deadlock.
Finally, we note that in various instances one observes a rather large number of abstraction/refinement
iterations over a relatively small state space. This occurs because our initial abstraction is very small (asingle state) and the successive refinement steps are designed to minimize the increase of the state space. We
expect that different choices of initial abstraction and a more aggressive refinement strategy would lead to
fewer iterations. The approach we followed is chiefly aimed at mitigating the state-space explosion problem.

11. Conclusion and Future WorkIn this paper, we have presented an expressive framework for modelling and verifying linear-time temporal
specifications on concurrent software systems. Our approach involves both states and events, and is predicatedon a compositional counterexample-guided abstraction refinement scheme. We have also shown how standard
automata-theoretic techniques for verifying linear temporal logic formulas can be ported to our frameworkat no extra cost, and have implemented these within our C model checker magic. We have also carried out
a number of experiments on industrial benchmarks, and have discovered bugs in the real-time operating
system Micro-C/OS. These experiments have led us to conclude that not only does a state/event formalism
facilitate the formulation of appropriate specifications (as compared to standard pure state-based or eventbased frameworks), but also yields substantial improvements in both verification time and memory usage.
We have also presented a new algorithm to detect deadlocks in concurrent blocking message-passing
programs. This algorithm not only complements our state/event verification framework, but is also highly
useful in its own right. Once again, the strength of our approach resides in the use of efficient abstractions
as well as compositional reasoning, despite the fact that deadlock is non-compositional and moreover is notpreserved by classical abstractions. Our technique is automated and employs iterative abstraction refinement
to scale to real-life examples. Experimental results demonstrate the effectiveness of our approach on industrial
benchmarks. We believe it can be improved further by using assume-guarantee style reasoning, and we plan
to investigate this issue in the future.
There remain many other avenues for further research. In our current framework, it may be possible tofurther optimize the automata-theoretic part of the verification, by directly transforming SE-LTL formulas into labelled Büchi automata. Doing so should yield more compact automata-based representations ofspecifications, resulting in a smaller overall state space. Another direction is to investigate other, more aggressive (and perhaps specification-dependent), notions of abstraction. magic is at present an explicit model
checking tool—it could be worthwhile to incorporate symbolic and partial order techniques to improve its
efficiency further. Finally, an interesting area of research is to develop mechanisms to handle shared variables
compositionally.

References[ABB][ACFM85]

ABB website. http://www.abb.com.
T. S. Anantharaman, E. M. Clarke, M. J. Foster, and B. Mishra. Compiling path expressions into VLSI circuits.
In Proceedings of the 12th Annual ACM Symposium on Principles of Programming Languages (POPL), pages
191–204. ACM Press, 1985.
[AQR+ 04] T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: A model checker for concurrent software. In
Proceedings of the 16th International Conference on Computer Aided Verification (CAV), volume 3114 of Lecture
Notes in Computer Science, pages 484–487. Springer, 2004.
[BLAST]
BLAST website. http://www-cad.eecs.berkeley.edu/∼rupak/blast.
[BLO98]
S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems compositionally andautomatically. In Proceedings of the 10th International Conference on Computer Aided Verification (CAV), volume1427 of Lecture Notes in Computer Science, pages 319–331. Springer, 1998.
[BMMR01] T. Ball, R. Majumdar, T. D. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In
Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages
203–213. ACM Press, 2001.
[BR91]
S. D. Brookes and A. W. Roscoe. Deadlock analysis of networks of communicating processes. Distributed Computing, 4:209–230, 1991.

22[BR01]

Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha

T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In Proceedingsof the 8th International SPIN Workshop, volume 2057 of Lecture Notes in Computer Science, pages 103–122.
Springer, 2001.
[Bro89]M. C. Browne. Automatic verification of finite state machines using temporal logic. PhD thesis, Carnegie Mellon
University, 1989. Technical report no. CMU-CS-89-117.
[BS01]
J. Bradfield and C. Stirling. Modal Logics and Mu-Calculi: An Introduction, pages 293–330. Handbook of Process
Algebra. Elsevier, 2001.
[Bur92]
J. Burch. Trace algebra for automatic verification of real-time concurrent systems. PhD thesis, Carnegie Mellon
University, 1992. Technical report no. CMU-CS-92-179.
[CC77]
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the SIGPLAN Conference on Programming Languages,
1977.
[CCG+ 03] S. Chaki, E. M. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. In
Proceedings of the 25th International Conference on Software Engineering (ICSE), pages 385–395. IEEE Press,
2003.
[CCG+ 05] S. Chaki, E. M. Clarke, O. Grumberg, J. Ouaknine, N. Sharygina, T. Touili, and H. Veith. An expressive verification
framework for state/event systems. In Proceedings of the 5th International Conference on Integrated Formal
Methods (IFM), Lecture Notes in Computer Science. Springer, 2005.
[CCK+ 02] P. Chauhan, E. M. Clarke, J. H. Kukula, S. Sapra, H. Veith, and D. Wang. Automated abstraction refinement formodel checking large state spaces using SAT based conflict analysis. In Proceedings of 4th International Conference
on Formal Methods in Computer-Aided Design (FMCAD), volume 2517 of Lecture Notes in Computer Science,
pages 33–51. Springer, 2002.
[CCO+ 04] S. Chaki, E. M. Clarke, J. Ouaknine, N. Sharygina, and N. Sinha. State/event-based software model checking.
In Proceedings of the 4th International Conference on Integrated Formal Methods (IFM), volume 2999 of Lecture
Notes in Computer Science, pages 128–147. Springer, 2004.
[CCOS04] S. Chaki, E. M. Clarke, J. Ouaknine, and N. Sharygina. Automated, compositional and iterative deadlock detection.
In Proceedings of the 2nd ACM-IEEE International Conference on Formal Methods and Models for Codesign(MEMOCODE). IEEE Press, 2004.
[CDH+ 00] J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Păsăreanu, Robby, and H. Zheng. Bandera: extracting
finite-state models from Java source code. In Proceedings of the 22nd International Conference on Software
Engineering (ICSE), pages 439–448. ACM Press, 2000.
[CE81]
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal
logic. In Proceedings of the Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science,
pages 52–71. Springer, 1981.
[CES86]E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using
temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
[CGJ+ 00] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In
Proceedings of the 12th International Conference on Computer Aided Verification (CAV), volume 1855 of Lecture
Notes in Computer Science, pages 154–169. Springer, 2000.
[CGKS02] E. M. Clarke, A. Gupta, J. H. Kukula, and O. Strichman. SAT based abstraction-refinement using ILP and machinelearning techniques. In Proceedings of the 14th International Conference on Computer Aided Verification (CAV),
volume 2404 of Lecture Notes in Computer Science, pages 265–279. Springer, 2002.
[CGL94]E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Transactions on Programming
Languages and Systems, 16(5):1512–1542, 1994.
[CGP99]E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
[CGP03]J. M. Cobleigh, D. Giannakopoulou, and C. S. Păsăreanu. Learning assumptions for compositional verification.
In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of
Systems (TACAS), volume 2619 of Lecture Notes in Computer Science, pages 331–346. Springer, 2003.
[Cor96]James C. Corbett. Evaluating deadlock detection methods for concurrent software. Software Engineering,22(3):161–180, 1996.
[COYC03] S. Chaki, J. Ouaknine, K. Yorav, and E. M. Clarke. Automated compositional abstraction refinement for concurrent
C programs: A two-level approach. In Proceedings of the Workshop on Software Model Checking (SoftMC). ENTCS
89(3), 2003.
[Dil88]D. L. Dill. Trace theory for automatic hierarchical verification of speed-independent circuits. PhD thesis, Carnegie
Mellon University, 1988. Technical report no. CMU-CS-88-119.
[DIS99]C. Demartini, R. Iosif, and R. Sisto. A deadlock detection tool for concurrent Java programs. Software: Practice& Experience, 29(7):577–603, 1999.
[FHRR04] C. Fournet, C. A. R. Hoare, S. K. Rajamani, and J. Rehof. Stuck-free conformance. In Proceedings of the 16th
International Conference on Computer Aided Verification (CAV), volume 3114 of Lecture Notes in Computer
Science, pages 242–254. Springer, 2004.
[FSEL]
Formal Systems (Europe) Ltd. website. http://www.fsel.com.
[GL94]
O. Grumberg and D.E. Long. Model checking and modular verification. ACM Transactions on Programming
Languages and Systems, 16(3):843–871, 1994.
[GM03]
D. Giannakopoulou and J. Magee. Fluent model checking for event-based systems. In Proceedings of the 11th
ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE), pages 257–266. ACM Press, 2003.
[GPVW95] R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal

Concurrent Software Verification with States, Events, and Deadlocks[GS97][HJMQ03][HJMS02][HJS01][Hoa85][HQR00][Koz83][Kur89][Kur94][KV98][LBBO01][LP85][LTSA][MAGIC][McM97][MH00][Mil89][MJ97][NCOD97][NFGR93][NV95][PDV01][Pnu86][QS81][RD87][Ros97][SB00][SLAM][SSL]

23

logic. In Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing
and Verification, pages 3–18. Chapman & Hall, 1995.
S. Graf and H. Saı̈di. Construction of abstract state graphs with PVS. In Proceedings of the 9th International
Conference on Computer Aided Verification (CAV), volume 1254 of Lecture Notes in Computer Science, pages
72–83. Springer, 1997.
T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer. Thread-modular abstraction refinement. In Proceedingsof the 15th International Conference on Computer Aided Verification (CAV), volume 2725 of Lecture Notes in
Computer Science, pages 262–274. Springer, 2003.
T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Proceedings of the 29th Annual ACM
Symposium on Principles of Programming Languages (POPL), pages 58–70. ACM Press, 2002.
M. Huth, R. Jagadeesan, and D. Schmidt. Modal transition systems: A foundation for three-valued program
analysis. In Proceedings of the 10th European Symposium on Programming (ESOP), volume 2028 of Lecture Notes
in computer Science, pages 137–154. Springer, 2001.
C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
T. A. Henzinger, S. Qadeer, and S. K. Rajamani. Decomposing refinement proofs using assume-guarantee reasoning. In Proceedings of the International Conference on Computer-Aided Design (ICCAD), pages 245–252. IEEE
Computer Society Press, 2000.
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983.
R. P. Kurshan. Analysis of discrete event coordination. In Proceedings of the REX Workshop, volume 430 ofLecture Notes in Computer Science, pages 414–453. Springer, 1989.
R. P. Kurshan. Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton
University Press, 1994.
E. Kindler and T. Vesper. ESTL: A temporal logic for events and states. In Proceedings of the 19th International
Conference on the Application and Theory of Petri Nets (ICATPN), volume 1420 of Lecture Notes in Computer
Science, pages 365–383. Springer, 1998.
Y. Lakhnech, S. Bensalem, S. Berezin, and S. Owre. Incremental verification by abstraction. In Proceedings of the
7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
volume 2031 of Lecture Notes in Computer Science, pages 98–112. Springer, 2001.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification.
In Proceedings of the 12th Annual ACM Symposium on Principles of Programming Languages (POPL), pages
97–107. ACM Press, 1985.
LTSA website. http://www-dse.doc.ic.ac.uk/concurrency/ltsa/LTSA.html.
MAGIC website. http://www.cs.cmu.edu/∼chaki/magic.
K. L. McMillan. A compositional rule for hardware design refinement. In Proceedings of the 9th International
Conference on Computer Aided Verification (CAV), volume 1254 of Lecture Notes in Computer Science, pages
24–35. Springer, 1997.
J. M. R. Martin and Y. Huddart. Parallel algorithms for deadlock and livelock analysis of concurrent systems. In
Proceedings of Comm. Process Architectures, 2000.
R. Milner. Communication and Concurrency. Prentice-Hall International, 1989.
J. M. R. Martin and S. Jassim. A tool for proving deadlock freedom. In Proceedings of the 20th World Occam andTransputer User Group Technical Meeting, 1997.
G. Naumovich, L. A. Clarke, L. J. Osterweil, and M. B. Dwyer. Verification of concurrent software with FLAVERS.
In Proceedings of the 19th International Conference on Software Engineering (ICSE), pages 594–595. ACM Press,
1997.
R. De Nicola, A. Fantechi, S. Gnesi, and G. Ristori. An action-based framework for verifying logical and behaviouralproperties of concurrent systems. Computer Networks and ISDN Systems, 25(7):761–778, 1993.
R. De Nicola and F. Vaandrager. Three logics for branching bisimulation. Journal of the ACM, 42(2):458–487,
1995.
C. S. Păsăreanu, M. B. Dwyer, and W. Visser. Finding feasible counter-examples when model checking abstracted
Java programs. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS), volume 2031 of Lecture Notes in Computer Science, pages 284–298. Springer,
2001.
A. Pnueli. Application of temporal logic to the specification and verification of reactive systems: A survey of current
trends. In Current Trends in Concurrency, volume 224 of Lecture Notes in Computer Science, pages 510–584.
Springer, 1986.
J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Selected Papers fromthe First and the Second European Workshop on Application and Theory of Petri Nets, pages 337–350. Springer,
1981.
A. W. Roscoe and N. Dathi. The pursuit of deadlock freedom. Information and Computation, 75(3):289–327,
1987.
A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall International, 1997.
F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In Proceedings of the 12th International
Conference on Computer Aided Verification (CAV), volume 1855 of Lecture Notes in Computer Science, pages
248–263. Springer, 2000.
SLAM website. http://research.microsoft.com/slam.
OpenSSL. http://wp.netscape.com/eng/ssl3/ssl-toc.html.

24[Sto02][WRING]

Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha

S. D. Stoller. Model-checking multi-threaded distributed Java programs. International Journal on Software Tools
for Technology Transfer, 4(1):71–91, 2002.
Wring website. http://vlsi.colorado.edu/∼rbloem/wring.html.