A Monitoring and Checking Framework for Run-time Correctness Assurance

Computer systems are often monitored for performance evaluation and enhancement, debugging and testing, control or to check for the correctness of the system. Recently, the problem of designing monitors to check for the correctness of system implementation has received increased attention from the research community. Traditionally, verification has been used to increase the confidence that a system will be correct by making sure that a design specification is correct. However, even if a design has been formally verified, it still does not ensure the correctness of an implementation of the design. This is because the implementation often is much more detailed, and may not strictly follow the formal design. So, there is possibility for introduction of errors into an implementation of a design that has been verified. One way that people have traditionally tried to overcome this gap between the design and the implementation has been to test the implementation\u27s behavior on a pre-determined set of input sequences. This approach, however, fails to provide guarantees about the correctness of the implementation on all possible input sequences. Consequently, when a system is running, it is hard to guarantee whether the current execution of the system is correct or not using the two traditional methods. Therefore, the approach of continuously monitoring a running system has received much attention, as it attempts to overcome the difficulties encountered by the two traditional methods for checking the correctness of the current execution of the system. We describe a framework that provides assurance on the correctness of program execution at run-time. This approach is based on the Monitoring and Checking (MaC) architecture, and complements the two traditional approaches for ensuring that a system is correct, namely static analysis and testing. Unlike these approaches which try to ensure that all possible executions of the system are correct, this approach ensures only that the current execution of the system is correct. The MaC architecture consists of three components: filter, event recognizer, and runtime checker. The filter extracts low-level information, in the form of values of program variables, from the instrumented system code, and sends it to the event recognizer. From this low-level information, the event recognizer detects the occurrence of abstract events, and informs the run-time checker about these. The run-time checker then, based on the events, checks the conformance of the behavior of the system on the current execution, to the formal requirement specification for the system