|
Abstract : |
We consider symbolic verification for a class of parametrized systems, where a system consists of a linear array of processes, and where an action of a process may in general be guarded by both local conditions restricting the state of the process about to perform the action, and global conditions defining the context in which the action is enabled. Such a model captures the behaviour, e.g., of idealized versions of mutual exclusion protocols, such as the bakery and ticket algorithms by Lamport, Burn's protocol, Dijkstra's algorithm, and Szymanski's algorithm. The presence of both local and global conditions makes these protocols infeasible to analyze, using existing model checking methods for parametrized systems. In all these methods the actions are guarded only by local conditions involving the states of a finite set of processes. We perform verification using the standard symbolic reachability algorithm enhanced by an operation to speed up the search of the state space. The speed up operation computes the effect of an arbitrary number of applications of an action, rather than a single application. This is crucial for obtaining termination e.g. when applying the algorithm to the above protocols. We illustrate the use of our method through applications to Szymanski's algorithm and Lamport's bakery protocol. Note: The extended abstract contains, in addition to 10 pages of text, an appendix which may be read at the discretion of the program committee. 1, |
