SOCKET通信程序模型抽取及可靠性验证

• 作者: 余立全 肖攀 肖美华
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: socket 模型检测 模型抽取 形式化验证
• 年，卷（期）: 2012,（11）
• 所属期刊栏目: 软件工程
• 页码范围: 102-105,141
• 分类号: TP301.2
• 字数: 4509字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2012.11.024

摘要

形式化方法是验证并发系统可靠性和安全性的重要手段.对高级语言开发的并发系统自动抽取的模型进行形式化验证是模型检测技术领域中的一个研究热点.鉴于socket函数调用顺序不正确产生的运行时潜在问题(内存泄漏、死锁、边界数据丢失等),针对顺序结构的socket程序,通过描述Promela消息数据结构和通道,构建socket函数的Promela模型,定义socket函数到Promela映射规则,提出socket函数调用序列抽取算法及目标Promela模型生成算法,用线性时态逻辑(LTL)刻画socket函数调用顺序应满足的性质,开发基于SPIN的socket通信程序分析系统.实验结果表明,该系统能有效检测socket通信程序的运行时潜在问题.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	肖美华	华东交通大学软件学院	27	313	8.0	17.0
5	余立全	南昌大学信息工程学院	1	30	1.0	1.0
6	肖攀	南昌大学软件学院	1	30	1.0	1.0