| Whether the software is credible has become one of the crucial factors for the national economy and national defence etc., especially in some safety-critical fields such as the control of nuclear reactor, aerial navigation and railway attempter. These systems require absolute safety and no error is permitted, or else terrible result may occur. For example, Clayton Tunnel Accident in August 1861 just resulted from half-baked protocol. And on June 1996, Europe spaceflight department, rocket Ari-ane 501 exploded 37 seconds after being fired, due to the bugs in its specification and design of the control. Similar reports are common occurrences. How to ensure the dependability of these systems has become a focus problem in computer science and cybernetics field.According to statistics, in America, $3000 hundred million will be spent in employing programmer to deal with the bug, which took up 40%~60% of the whole development period. Although so much time and energy has been consumed in demolishing bugs, they can't ensure bugs are removed from the software.With the aim to ensure the credibility and safety of the software system radically, many computer scientists, including A. PnDeli, a gainer of Turing Award, believe that it is an important way to construct safe software through validating and analyzing the system by formal methods. Model checking technology is one of the validating ways. And SPIN, which is a gainer of Association for Computing Machinery Software Systems Award, is one of the most famous model checking tools.SPIN'S typical mode of working is to start with the specification of a high level model of a concurrent system, or distributed algorithm, typically using SPIN'S graphical front-end XSPIN. After fixing syntax errors, interactive simulation is performed until basic confidence is gained that the design behaves as intended. Then, SPIN is used to generate an optimized on-the-fly verification program from the high level specification. This verifier is compiled, with possible compile-time choices for the types of reduction algorithms to be used, and executed. If any counterexamples to the correctness claims are detected, these can be fed back into the interactive simulator and inspected in detail to establish, and remove, their cause.In the front of this paper, the history, development and characteristics of SPIN, a famous model detection tool, are introduced. Promela, the SPIN modeling language, is followed. The installation of UNIX edition SPIN PIN in Windows 2000 through Cygwin is discussed in this paper. As follows, AB-protocol is described and we found the false and the leak. Finally, the course of analyzing crypto protocol by Promela designing is pointed out, and the potential attack was found. This paper includes the main doing work, the deep technique, and the creative work as follows: SPIN is a model checker for the verification of concurrent algorithms systems, especially is that auxiliary tools for analyzing agreement consistency. In this paper we discuss that how to setup and use SPIN in the Win32 environment and in the Cygwin/Linux/Unix environment. The simplest way to use SPIN is to use XSPIN, which has graphical interfaces. Graphical interfaces run without using SPIN and choose corresponding orders of SPIN. XSPIN gets anticipant output-answers through running SPIN in the background. XSPIN knows when and how to compile the code and it also knows that how to run the code, so you needn't to remember all the parameters. The paper introduces how to install and use XSPIN, the GUI of SPIN, on Cygwin platform. Promela (Protocol/Process Meta Language) is a formal descriptive language, which is written to make model of the finite states system. The paper introduces how to describe a... |
PDF Full Text Request