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

Model Extraction and Reliability Verification on SOCKET Communication Program

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

Formal method is a means to verify the reliability and safety of concurrent systems.Formal verification of model which is automatically extracted from concurrent system built from high level language is a hot research topic in the field of model checking technology.With the focus on potential run time problems（deadlocks,memory leaks,the boundary data loss and other run-time errors） result from abnormal socket function call sequence,this paper analyzed the sequence structure of the socket program,constructed the Promela model of socket functions through the description of message data structures and channels,defined mapping rules of socket function to Promela,proposed the socket function call sequence extraction algorithm and target Promela model generation algorithm,used linear temporal logic（LTL） to describe the property the socket function call sequence shall meet.A socket communication program analysis system was constructed.The experiment result shows that the system can detect the potential run time problems of socket program effectively.