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

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

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.