Specification and Verification of Dynamic Properties in Distributed Computations
Specification and Verification of Dynamic Properties in Distributed Computations
复制标题
DOI：
10.1006/jpdc.1995.1098
复制
发表时间：
1995-08
期刊：
影响因子：
--
通讯作者：
Özalp Babaoglu;M. Raynal
中科院分区：
文献类型：
--
作者：
Özalp Babaoglu;M. Raynal
指定和验证计算的动态属性的能力对于确定分布式应用程序的正确性至关重要。在这篇文章中，我们考虑了可以被编码为全局系统状态上的一般布尔谓词的性质。我们引入了两个全局谓词类，称为简单序列和区间约束序列，用于以某种保留因果关系的顺序指定期望状态以及插入不期望状态。我们的形式主义比更传统的提议更简单，并允许简洁和直观地表达许多有趣的系统属性。给出了在分布式计算中以在线和独立于观察者的方式验证这些谓词类的公式的算法。我们通过将我们的结果应用于分布式系统中的程序测试、调试和动态重新配置的例子来说明我们的结果的实用性。
The ability to specify and verify dynamic properties of computations is essential for ascertaining the correctness of distributed applications. In this paper, we consider properties that can be encoded as general Boolean predicates over global system states. We introduce two global 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 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.