| Analysis and validation of software systems is an important area of research in computer science. Traditionally, software engineers have tried, either to formally verify their design or test their system on a variety of inputs. In formal verification, one describes the program in some mathematical formalism and then tries to prove its correctness. Verifying systems does not guarantee correctness because it is the design, and not the implementation, that is verified, and because resource limitations prevent the verification of large systems. While testing, on the other hand, analyses an implementation of the software, it is often adhoc and fails to provide formal guarantees. Run-time analysis of systems attempts to address this problem, and this thesis examines the issues that arise in this area.; We investigate the problem of checking functional, terminating computation and monitoring reactive, non-terminating computation, separately. For functional computations, we extend work in the area of program checking by introducing a model of checking for approximate correctness, and design checkers under two different computational models. In spot checking, the checker is assumed to have random access to the bits of input-output pair of the program, while in stream checking, the checker streams through the input-output pair. The checkers that we describe are extremely efficient, in that they either don't even read the entire input-output pair, as in spot checking, or they use a very small amount of memory, as in stream checking.; We also provide a descriptive theory for the class of reactive languages that can be monitored. We show that this class of monitorable languages coincides with the class of the arithmetic hierarchy. We also characterize this class of languages using ω-automata with storage. We use this result to show that the system, MaC, that we developed, can monitor all these languages.; Finally, we describe the design and prototype implementation of a framework for monitoring and checking, called MaC. MaC integrates both functional checking and reactive system monitoring, and exploits the benefits that both these approaches offer. Moreover, MaC provides a framework to experiment with the theoretical ideas presented, on practical Java programs. |
