Abstract:

Runtime verification complements the two traditional approaches for ensuring that a system is correct, namely model checking and testing. Unlike these approaches which try to ensure that all possible executions of the system are correct, runtime verification concentrates on the correctness of the current execution of the system. This paper presents a runtime verification method based on the 3valued semantics. One hand, this method provides a complete solution from code instrumentation and system information extraction to monitor generation and verifying requirement specification against runtime tracing. On the other hand, the monitor based on the 3valued semantics has the ability to find the smallest good (bad) prefix, so the monitor can find the violation as early as possible. Meanwhile, we have developed the prototype tool and have applied it in an example.

Key words: 3valued semantic;runtime verification;monitor