A Software Runtime Verification Method Based on the 3-Valued Semantics
LI Bing-peng
Abstract
LI Bing-peng
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.
A significance statement is not available in the OpenAlex record.
A contribution statement is not available in the OpenAlex record.
Method details are not available in the OpenAlex metadata.
Findings are not separately available in the OpenAlex metadata.
Limitations are not available in the OpenAlex metadata.
Application details are not available in the OpenAlex metadata.
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 concepts: Computer science, Runtime verification, Correctness, Programming language, Semantics (computer science), Software verification, Functional verification, Tracing