Monitoring and Checking of Distributed Systems with respect to Formal Specifications

University Of Illinois At Urbana-Champaign, Urbana IL

Investigators

Abstract

Proposal Number: 0429639 TITLE: Monitoring and Checking of Distributed Systems with Respect to Formal Specifications PI: Mahesh Viswanathan Our 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 to develop tools and algorithms to automatically monitor distributed systems with respect to formal specifications. In order to overcome the state space explosion problem encountered in distributed debugging, the PI plans to partial-order techniques in centralized monitoring and game-theoretic ideas to construct local decentralized monitors from global specifications.