The Socket Communication Program Analysis System Based On SPIN

Formal method is a means to verify the reliability and safety of concurrent systems. Model checking is used for formal verification of finite state concurrent (distributed) systems, and has been applied to a variety of software safety and reliability verification. Extracting the model from the concurrent software systems built with high-level language and using the model checking tool to verify the extracted model is a hot research topic in model checking technology. The reliability of socket communication program based on TCP/IP protocol is an important foundation of the Internet data transmission. This paper, with its focus on the reliability of socket communication program developed in C language, explores the technology of socket communication program analysis and verification based on model checking tool SPIN. The following are the main tasks and achievements:1. This paper is to analyze the correctness of the socket function call order in the socket communication program. That is to detect the potential run time problems (deadlocks, memory leaks, the boundary data loss and other run-time errors) result from abnormal socket function call sequence in the server and client socket program.2. With the focus on the correctness of the socket function call sequence, design a scheme for extracting model from the source code of the socket program; analyze the sequence structure of the socket program and propose the socket function call sequence extraction algorithm; define the Promela message data structures and channels; specify the Promela model of socket function; define mapping rules of socket function to Promela; propose target Promela model generation algorithm, and use linear temporal logic (LTL) to describe the model property.3. Use the sequence of atomic, partial order reduction, bit-state hashing strategy to improve the efficiency in verification and compress the state space and storage space in the process of verification.4. Design and implement the socket communication program analysis system. The system can detect run-time problems which result from the use of improper socket function call order. If there are loopholes in the system, it is able to graphically display the code execution path. The system has the abstract, generality, scalability, efficiency, practicality, and can be used as an effective aid to the design of socket communication program.