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

• 作者: 朱云龙 王哲民 陈哲 黄志球
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 运行时验证 形式化规约 层次哈希森林 有限状态自动机
• 年，卷（期）: 2016,（12）
• 所属期刊栏目: 计算机软件与数据库研究
• 页码范围: 2667-2672
• 页数: 6页
• 分类号: TP311
• 字数: 7709字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈哲		5	13	2.0	3.0
2	朱云龙	南京航空航天大学计算机科学与技术学院	2	9	2.0	2.0
3	王哲民	南京航空航天大学计算机科学与技术学院	3	9	2.0	3.0
4	黄志球		7	13	2.0	3.0