Monitoring and Checking of Distributed Systems with respect to Formal Specifications

提案号：0429639标题：关于正式规范的分布式系统的监控和检查我们对计算机和数字系统的日益依赖，需要对底层软件的可靠性的关键需求。然而，开发正确软件的任务特别困难，因为现代软件系统需要处理复杂的问题。因此，越来越需要自动化技术来持续分析软件。传统的分析程序正确性的方法，即形式验证和测试，在几个方面是不够的。特别地，验证是在系统的正式设计上执行的，而不是它的实现，而测试通常是临时的，不能提供正式的保证。在运行时监视和检查系统可以尝试解决这些问题。尽管在开发监测工具方面取得了很大进展，但有一个根本性的挑战限制了它们的广泛适用性。大多数监控系统只分析单处理器系统或具有同步全局时钟的系统。在这个项目中，PI计划开发工具和算法来根据正式规范自动监控分布式系统。为了克服分布式调试中遇到的状态空间爆炸问题，PI计划将集中监控中的部分顺序技术和博弈论思想结合起来，从全局规范构建局部分散监控。

Proposal Number: 0429639TITLE: Monitoring and Checking of Distributed Systems with Respect to Formal SpecificationsPI: Mahesh ViswanathanOur increasing reliance on computer and digital systems, necessitates the critical need for the reliability of the underlying software. However, the task of developing correct software is particularly difficult since modern software systems need to address complicated problems. Hence there is an increasing need for automated techniques to analyze software continually. Traditional methods for analyzing the correctness of programs, namely, formal verification and testing are inadequate in several respects. In particular,verification is performed on the formal design of a system and not its implementation, while testing is often ad hoc and fails to provide formal guarantees. Monitoring and checking systems at run-time attempts to address these concerns. Although great strides have been made in developing monitoring tools, there is one fundamental challenge that limits their widespread applicability. Most of the monitoring systems only analyze uni-processor systems or systems that have a synchronized global clock. In this project, the PI plans todevelop tools and algorithms to automatically monitor distributed systems with respect to formal specifications. In order to overcome the state space explosion problem encountered in distributeddebugging, the PI plans to partial-order techniques in centralized monitoring and game-theoretic ideas to construct local decentralized monitors from global specifications.