Authors: Henrik E. Jensen and Nancy A. Lynch
Appears: Proceedings Tools and Algorithms for the Construction and Analysis of Systems, 4th International Conference, TACAS'98, Lisbon, Portugal, March/April 1998.
Abstract: Within the Input/Output Automata framework, we state and prove a general abstraction theorem giving conditions for preservation of safety properties from one automaton to another. We use our abstraction theorem to verify that Burns distributed mutual exclusion algorithm parameterized in the number of processes n satisfies the mutual exclusion property. The concrete n-process algorithm is abstracted by a simple 2-process algorithm which is property preserving with respect to the mutual exclusion property. The condition for property preservation is proved to be satisfied by use of the LP theorem prover with a minimum of user assistance, and the 2-process abstraction is automatically verified using the SPIN model checker.