Formal specification, based on critical mathematics, not only make the process of software development more effective and precise, but also contain a great deal of information that can be as the original reliable basis for the generation of test sequences. The work reported here base on the standard B notation, splitting the operation to the equal effect predications and then generate state transition diagram according to path coverage criterion, and also solving the indeterminism of state transition. Generating the test sequences according to the test criterion on the state diagram, which can prove an effective test, has also been presented.