Abstract: 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 func- tion 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.

Key words: Socket, Model checking, Model extraction, Formal verification