Parameterized Model Checking of Protocols: Two Developments

Опубликовано 6 сентября 2016, 5:03

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.