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