\input zb-basic
\input zb-ioport
\iteman{io-port 05473988}
\itemau{Babaoglu, Oezalp; Raynal, Michel}
\itemti{Specification and verification of dynamic properties in distributed computations.}
\itemso{J. Parallel Distrib. Comput. 28, No. 2, 173-185 (1995).}
\itemab
Summary: The ability to specify and verify dynamic properties of computations is essential for ascertaining the correctness of distributed applications. We consider properties that can be encoded as general Boolean predicates over global system states. We introduce two global predicate classes called ${\it $simple sequences} and ${\it $interval-constrained sequences} for specifying desirable states in some causality-preserving order along with intervening undesired states. Our formalism is simpler than more traditional proposals and permits concise and intuitive expression of many interesting system properties. Algorithms are given for verifying formulas belonging to these predicate classes in an on-line and observer-independent manner during distributed computations. We illustrate the utility of our results by applying them to examples drawn from program testing, debugging, and dynamic reconfiguration in distributed systems.
\itemrv{~}
\itemcc{F.1.2 F.3.1 D.2.1 D.2.4 I.2.2}
\itemut{simple sequences; interval-constrained sequences}
\itemli{doi:10.1006/jpdc.1995.1098}
\end