参数化运行时验证研究和工具实现

摘要 随着软件规模的不断增大，如何保证软件的可靠性和安全性成为学术界和工业界越来越关注的问题.运行时验证是一种新型的程序自动验证技术，弥补了静态分析和模型检测等常用方法的缺点.设计一种针对C程序的监控器规约语言，用于描述针对C程序的形式化规约.该语言支持基于有限状态自动机和正则表达式的参数化运行时验证.本文借助开源工具flex和bison实现了支持该语言的参数化运行时验证工具MOVEC.为了对运行时产生的大量监控器进行索引，我们提出并实现了一种层次哈希森林的数据结构.实验证明该工具是可行且高效的.