基于三值语义的软件运行时验证方法

A Software Runtime Verification Method Based on the 3-Valued Semantics

运行时验证技术是对传统的程序正确性保证技术如模型检验和测试的有效补充。模型检验和测试都试图验证系统的所有可能执行路径的正确性,而运行时验证关注的是系统的当前执行路径。本文提出一种基于三值语义的软件运行时验证方法,一方面该方法提供了从代码插装、系统底层信息提取到监控器生成、验证系统运行轨迹是否满足性质规约的完整的解决方案;另一方面基于三值语义的监控器有发现一条无穷运行轨迹的最小好(坏)前缀的能力,从而使得监控器能尽可能早的发现性质违背。同时,我们开发了基于三值语义的软件运行时验证原型工具并针对案例进行了分析。

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.