Abstract

Research on formal methods for software has concentrated on verifying code and formally developing code from specifications. However, there may also be other routes that formal methods can follow to become part of standard practice in software development. We report on research into applying the technique of log file analysis for checking test results to a broad range of testing and other tasks. In this technique, we write a formally-defined program which can be used to analyze "log file" output of the software under test, to see if the log file reveals any faults in the software. The studies undertaken include applying the technique to both unit- and system-level testing and to requirements of both safety-critical and non-critical systems, and the use of log file analysis in combination with other testing methods. We also report on the technique of using log file analyzers to simulate the software under test, both in order to validate the analyzers and to clarify requirements.