Analyzing And Verifying Network Protocols By Model Checking

The features of network protocols, such as distributed, concurrency and asynchronous, make it hard to reproduce some errors by traditional test. Model checking is a formalized verification method. It can automatically verify whether a system is meeting their specifications. It has many advantages. Such as it is fully automatic, and also can provide error trace. It is widely used in harware and software verifications.Model checking is helpful to find errors in the design of protocols.In this paper, we presented the formal verified of network protocols by model checker SPIN. We extracted formal models from TCP connection management protocol and 802.11i authenticate protocol. After analyzed the RFC documents, we constracted finite state automaton as the middle models.The finite state automaton models were transformed to PROMELA, the input language to SPIN. Then some properties were represented by Linear-time Temporal Logic (LTL) formula. The simulation results were used to repair the modles. Some important properties were verified by SPIN.The error traces were used to locating errors. We uncovered some probems in TCP connection procedure and 802.11i protocol, and corrections to these errors have been proposed.In this paper, we modeled and verified real protocols.A modeling framework based on decomposition and iteration was present. This framework was helpful to control the size of the model. The models and verified results are helpful to understand protocol design.