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

作     者：肖美华 余立全 肖攀 XIAO Mei-hua;YU Li-quan;XIAO Pan

作者机构：华东交通大学软件学院南昌330013 南昌大学信息工程学院南昌330031 南昌大学软件学院南昌330047 

出 版 物：《计算机科学》 (Computer Science)

年 卷 期：2012年第39卷第11期

页      面：102-105,141页

核心收录：

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金项目(61163005) 中国博士后科学基金(20110491497) 江西省自然科学基金项目(2007GZS1844 2010GZS0150) 江西省科技支撑计划(2009BGB01600) 江西省软科学项目(2010DRB01400) 江西省教育厅科技研究项目(GJJ09050)资助 

主　　题：socket 模型检测 模型抽取 形式化验证 

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