CAREER: Monitoring and Assertion-Checking for Internet-Scale Applications

这个CAREER奖的总体目标是开发一个互联网规模的在线预测评估。 该项目的第一个具体目标是验证互联网的部分同步模型。 第二个具体目标是开发可扩展的监测和谓词评估算法，该算法通过聚合信息来利用层次结构，近似控制保真度和性能之间的权衡，将子谓词的评估分布到局部域，在该局部域中将利用部分同步假设。符号模型检查和偏序方法提高了域内监控的性能。 最后，组合推理技术和数据聚合将用于执行域间监控。 所提出的研究的预期结果是一组强大的和可扩展的算法来评估系统状态的正确性保证建立验证同步假设。 这项研究预计将提供一个基本的能力来理解分布式系统的行为，使用的技术是正式的正确和实用的，适用于网格计算，大规模的协作系统，和复制的服务器。 教育目标是通过参与研究，通过对计算机科学的广泛介绍，以及通过发展与计算机科学相关的学术准备，明确教授教育成功技能，从而提高代表性不足的学生在计算机科学领域的保留率和成功率。这些活动将在亲和团体模式的范围内进行。 预计这种参与将通过发展亲和力和持久性，导致更大的保留和成功。

The overall objective of this CAREER award is the development of an Internet-scale, on-line predicate-evaluation. The first specific objective of the project is the validation of a partial synchrony model for the Internet. The second specific objective is the development of scalable monitoring and predicate-evaluation algorithms which exploit hierarchy by aggregating information, approximating to control of the tradeoff between fidelity and performance, distributing the evaluation of sub-predicates to local domains, within which partial synchrony assumptions will be exploited within. Symbolic model-checking and partial order methods enhance the performance of intra-domain monitoring. Finally, compositional reasoning techniques and data aggregation will be used to perform inter-domain monitoring. The expected result of the proposed research is a set of robust and scalable algorithms to evaluate system state with correctness guarantees established with respect to validated synchrony assumptions. This research is expected to provide a fundamental ability to understand the behavior of a distributed system using techniques that are formally correct and practical, suitable for Grid computing, large-scale collaboration systems, and replicated servers. The educational objective is to increase in the retention and success of underrepresented students in computer science by explicitly teaching educational success skills through participation in research, through a broad-spectrum introduction to computer science, and through development of academic preparedness specifically relevant to computer science. These activities will take place within the context of the affinity group model. It is expected that such participation will lead to greater retention and success through the development of affinity and persistence.