Parameterized Model Checking of Protocols: Two Developments

July 22, 2004
Jesse Bingham | University of British Columbia

This talk will consist of two somewhat independent sub-talks. Both discuss research motivated by parameterized model checking of shared-memory protocols, but they are somewhat orthogonal.

In the first part we consider the problem of automatically verifying sequential consistency of a shared-memory multiprocessor for an arbitrary number of addresses and data values by model checking. This problem is nontrivial since checking sequential consistency cannot be reduced to observing a single address.

We leverage real-world assumptions, automatic abstraction, and previous sequential consistency verification techniques. The approach is applied successfully to two different shared-memory protocols.

The second part will discuss a novel approach to computing backward reachability from an upward-closed set in a class of parameterized systems that includes broadcast protocols and petri nets. In contrast to the standard approach, which performs a single least fixpoint computation, we consecutively compute the finite state least fixpoint for constituents of increasing size, which allows us to employ binary decision diagram (BDD)-based symbolic model checking. In support of this framework, we prove a necessary and sufficient condition for convergence and intersection with the initial states, and provide an algorithm that uses BDDs as the underlying data structure. We give experimental results that demonstrate the existence of a petri net for which our algorithm is two orders of magnitude faster than the standard approach, and speculate properties that might suggest which approach to apply.

Speaker Details

Jesse Bingham is a PhD candidate in the Department of Computer Science at UBC, and is co-supervised by Anne Condon and Alan Hu. His primary research interests lie in algorithmic verification of complex systems such as shared memory protocols, software, hardware, and parameterized systems. Specifically, his Ph.D. research pertains to the problem of using model checking techniques for the verification of the sequential consistency memory model. This work includes identification of decidable variants of sequential consistency, and tackling the parameterized model checking problem with respect to this property.He is currently on a summer internship at Microsoft Research in Silicon Valley, and hopes to graduate by summer 2005.