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

J4 ›› 2011, Vol. 33 ›› Issue (10): 99-104.

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

隋〓平1,赵常智1,董〓威1,李冰鹏2

（1.国防科学技术大学计算机学院，湖南长沙 410073;2.南京政治学院上海分院，上海 200433)

收稿日期:2010-05-20 修回日期:2010-10-26 出版日期:2011-10-25 发布日期:2011-10-25

A Software Runtime Verification Method Based on the 3Valued Semantics

SUI Ping1,ZHAO Changzhi1,DONG Wei1,LI Bingpeng2

(1.School of Computer Science,National University of Defense Technology,Changsha 410073;2.Shanghai Branch,Nanjing Political College,Shanghai 200433,China)

Received:2010-05-20 Revised:2010-10-26 Online:2011-10-25 Published:2011-10-25

摘要/Abstract

摘要：

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

关键词: 三值语义, 运行时验证, 监控器

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

隋〓平1,赵常智1,董〓威1,李冰鹏2. 基于三值语义的软件运行时验证方法[J]. J4, 2011, 33(10): 99-104.

SUI Ping1,ZHAO Changzhi1,DONG Wei1,LI Bingpeng2. A Software Runtime Verification Method Based on the 3Valued Semantics[J]. J4, 2011, 33(10): 99-104.

[1]	张可迪,舒绍娴,董威. 一种嵌入式操作系统运行时验证方法[J]. J4, 2014, 36(05): 900-905.
[2]	刘晓建,戴华东,颜跃进. VMSF—一种内核级虚拟机监控器调度框架[J]. J4, 2012, 34(2): 78-81.