Colloquium Speaker

Speaker:		Mahesh Viswanathan University of Pennsylvania
Topic:		Dynamic Analysis of Software Systems
Date:		Thursday, March 23, 2000
Time:		11:00 AM
Place:		Gould-Simpson, Room 701

ABSTRACT

As our reliance on computers and digital systems increases, the need for the underlying software to be dependable becomes critical. Hence, there is an increasing need for automated techniques to analyze and validate software. While much research in the past two decades has addressed ensuring software reliability, the traditionally dominant themes of work, namely, formal verification and testing are inadequate methodologies in several respects. In particular, verification is performed on the formal design of systems and not its implementation. Since the construction of the software from the design is a manual, error-prone process, correctness of the design fails to provide an accurate measure of the performance of the actual software. On the other hand, though testing is performed on the system implementation, it is often ad hoc and fails to provide formal guarantees. Monitoring and checking program behavior at run-time attempts to address these concerns, and this talk will examine some of the issues that arise in this approach.

We will begin by investigating the problem of checking functional, terminating computation. We will extend prior models of program checking to incorporate the notion of approximate correctness, and demonstrate pragmatic problems for which these models permit highly efficient algorithms for checking. We will then examine the problem of monitoring non-terminating, concurrent, reactive systems. We will present MaC, a software tool that automatically instruments and dynamically checks JAVA byte-code, based on correctness requirements written in a language similar to linear temporal logic. We will demonstrate the usefulness of MaC by presenting results on analyzing simulations of network protocols.