Test Case Generator for Campus-wide Card System Based on Object-Z and Markov

For improving the accuracy and reliability of the Campus card system test requirement, test cases generator based on Object-Z and Markov chain is proposed in this paper.The formal specification of the system is gained by using Object-Z, then test scenarios and operation sequence diagrams are generated.Operation sequence diagrams are converted into a Markov chain usage model.According to the test scenarios and the Markov chain model to produce a relatively reasonable amount of test cases.The method don't need to run the system, and could be able to test the functionality of the system in the time of requirements analysis.The results of generated test cases for campus-wide card system show the method is effective, and using the Markov chain ensures the reliability of the system test.