SPECIFICATION AND VERIFICATION OF DYNAMIC PROPERTIES IN DISTRIBUTED COMPUTATIONS

The ability to specify and verify dynamic properties of computations i s essential for ascertaining the correctness of distributed applicatio ns. In this paper, we consider properties that can be encoded as gener al Boolean predicates over global system states. We introduce two glob al predicate classes called simple sequences and interval-constrained sequences for specifying desirable states in some causality-preserving order along with intervening undesired states. Our formalism is simpl er than more traditional proposals and permits concise and intuitive e xpression of many interesting system properties. Algorithms are given for verifying formulas belonging to these predicate classes in an on-l ine and observer-independent manner during distributed computations. W e illustrate the utility of our results by applying them to examples d rawn from program testing, debugging, and dynamic reconfiguration in d istributed systems. (C) 1995 Academic Press, Inc.