Verification of progress properties in a shared-memory concurrent system represented as a labeled transition system

Martti Tienari and Päivi Kuuppelomäki: Verification of progress properties in a shared-memory concurrent system represented as a labeled transition system Report C-2000-3, Department of Computer Science, University of Helsinki, February 2000. 26 pages. <http://www.cs.helsinki.fi/TR/C-2000/3>

Full paper: Postscript file

Abstract

A shared memory concurrent system can be modeled as a labeled transition system. The system is assumed to be finite. Verification of progress properties of this kind of system is studied.

We present methods to check "leads-to" type of progress properties from global state graphs for both weakly and strongly fair executions. We also study a new method, applicable for two-process systems under weak fairness, to check progress properties of a system from the corresponding bisimilar minimized system. A novel divergence preserving bisimilarity is needed to make this possible. Two simple mutual exclusion protocols are analyzed to demonstrate the workings of the latter method.

Index Terms

Categories and Subject Descriptors:
F.3.1 [Logics and meanings of programs]: Specifying and Verifying and Reasoning about Programs
D.2.4 [Software engineering]: Software/Program Verification

General Terms: Verification

Additional Key Words and Phrases: Equivalences, Fairness, Labeled Transition System, Liveness