Model Extraction and Reliability Verification on SOCKET Program

Abstract:

Formal method is a means to verify the reliability and safety of concurrent systems. Formal verification of model which 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, we analyze the sequence structure of the socket program and construct the Promela model of socket functions through the description of message data structures and channels, as well as define mapping rules of socket function to Promela. The socket function call sequence extraction algorithm and target Promela model generation algorithm are proposed by using linear temporal logic (LTL) to describe the property the socket function call sequence. A socket communication program analysis system has been constructed. The experiment result shows that the system can detect the potential run time problems of socket program effectively.

• Periodical: Advanced Materials Research (Volumes 616-618)
• Pages: 2055-2059
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.616-618.2055
• Online since: December 2012
• Authors: Min Luo
• Keywords: Formal Verification, Model Checking, Model Extraction, Socket

References

[1] Pedro de la Cámara. Checking the reliability of socket based communication software[J]. Int J Softw Tools Technol Transfer, 2009, 11:359-374.

DOI: 10.1007/s10009-009-0112-7

[2] Martinez, J., Jimenez, C. Software model checking for Internet protocols with java pathfinder[C]. 6th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, 2008, pp.91-100.

DOI: 10.5220/0001738600910100

[3] Quan Jia-hui, Zhang Huan-huan.Verification and Improvement of MINIX 3 Based on FeaVer [J]. Computer Engineering,2010,36(22):46-48.

[4] Gerard J. Holzmann, Margaret H. Smith. Software model checking: extracting verification models from source code [J]. software testing, verification and reliability, 2001, 11:65-79.

DOI: 10.1002/stvr.228

[5] Klaus Havelund, Thomas Pressburger, Model Checking Java Programs Using Java PathFinder[J]. Int J STTT, 2000, 2:366-381.

DOI: 10.1007/s100090050043

[6] James C. Corbett, Matthew B. Dwyer. Bandera: extracting finite state models from java source code [C]. Software Engineering, 2000, 439-448.

DOI: 10.1145/337180.337234

[7] Wang Da-wei, Zhang Da-fang. A Pract ical Method for Automat ically Model Checking the ANSI-C Programs [J]. Computer Eegineering & Science, 2010,32(4) 79-82.

[8] W. Richard Stevens. TCP/IP Illustrated, Vol 1: The Protocols[M]. Beijing: Posts&Telecm Press, 2010.

[9] W. Richard Stevens. TCP/IP Illustrated, Vol 2: The Implementation[M]. Beijing: Posts&Telecm Press, 2010.

[10] W.Richard Stevens. Advanced Programming in the UNIX Environment Second Edition[M], Beijing: Posts&Telecm Press, 2010.

[11] Xiao Mei-Hua, Xue Jin-Yun, Verification of Concurrent Systems Using SPIN/Promela[J]. Computer Engineering, 2004, 31(8): 201-203.

[12] G.J. Holzmann, The SPIN Model Checker, Primer and Reference Manual [M]. Addison-Wesley, 2003.