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

Research on Parametric Runtime Verification and Tool Implementation

作　　者：王哲民[1,2] 陈哲[1,2] 朱云龙[1,2] 黄志球[1,2] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106 [2]软件新技术与产业化协同创新中心,南京211106

出　　处：《小型微型计算机系统》2016年第12期2667-2672,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61100034)资助;教育部留学回国人员科研启动基金项目(2013)资助

摘　　要：随着软件规模的不断增大,如何保证软件的可靠性和安全性成为学术界和工业界越来越关注的问题.运行时验证是一种新型的程序自动验证技术,弥补了静态分析和模型检测等常用方法的缺点.设计一种针对C程序的监控器规约语言,用于描述针对C程序的形式化规约.该语言支持基于有限状态自动机和正则表达式的参数化运行时验证.本文借助开源工具flex和bison实现了支持该语言的参数化运行时验证工具M OVEC.为了对运行时产生的大量监控器进行索引,我们提出并实现了一种层次哈希森林的数据结构.实验证明该工具是可行且高效的.With the increasing of the scale of software, how to guarantee the reliability and safety of the software has become a growing concern in academia and industry. Runtime verification is a new type of automatic program verification technology, which makes up for the shortcomings of static analysis and model checking. This paper designs a monitor specification language for C programs ,which is used to describe the formal specification for C programs. This language supports the parametric runtime verification based on finite state machines and regular expressions. This paper implements the parametric runtime verification tool MOVEC which supports this language with the help of open source tool flex and bison. In order to index the large number of monitors generated at run time, we propose and implement a data structure of hierarchical hash table forest. Experiments show that the tool is feasible and effective.

关 键 词：运行时验证 形式化规约 层次哈希森林 有限状态自动机 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]