Usage modeling through sequence enumeration for automated statistical testing of a GUI application

Markov chain usage-based statistical testing has been an effective means in the economical production of high quality software that also provides credible evidence to support its dependability. Sequence-based specification is a rigorous specification method that derives a formal system model from informal functional requirements, which can be used as a formal method to construct a Markov chain usage model for statistical testing. This paper demonstrates a case study in which we apply these two methods in conjunction with supporting tools towards fully automated statistical testing of a GUI application. Preliminary results are promising.