Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem
Springer Berlin Heidelberg, Jan 24, 1996 - Computers - 143 pages
This monograph is a revised version of the author's Ph.D. thesis, submitted to the University of Liège, Belgium, with Pierre Wolper as thesis advisor.
The general pattern of this work, is to turn logical and semantic ideas into exploitable algorithms. Thus, it perfectly fits the modern trend, viewing verification as a computer-aided activity, and as algorithmic as possible, not as a paper and pencil one, dealing exclusively with semantic and logical issues. Patrice Godefroid uses state-space exploration as the key technique, which, as such or elaborated into model checking, is attracting growing attention for the verification of concurrent systems. For most realistic examples, the methods presented provide a significant reduction of memory and time requirements for protocol verification.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Concurrent Systems and Semantics
Using Partial Orders to Tackle State Explosion
7 other sections not shown
Other editions - View all
active(t Algoi(t algorithm of Figure automata backtracked Biichi automaton Chapter communication protocols computed by Algorithm Computer Aided Verification Computer Science computing persistent sets concurrent executions concurrent systems conditional dependency relation conditional stubborn set Consider deadlock defined Definition 4.15 Definition 6.2 dependent in sn depth-first search do-not-accord E.M. Clarke Elounda enabled transitions FIFO finite global state space Hence independent transitions interleavings Lemma LFCS model checking nonempty number of transitions operation on object opi and op2 partial order partial-order methods persistent-set selective search possible pre(t Proceedings process Pi proof protocol proviso of Definition PS+SLEEP reachable reduced state space relations can-be-dependent returned by Algorithm s.Sleep safety properties search using persistent semantics sequence of transitions set of transitions sets and sleep sleep set associated sn+i Stack state-space caching step 2.a stored strongly connected component temporal logic Theorem TMSCC trace automaton transition tj used(t valid conditional dependency weakly uniform