Monitoring and Checking of Distributed Systems with respect to Formal Specifications

点击翻译按钮获取中文摘要

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.