Behavior checking of web applications after testing

Testing is the last step to check the correctness of a software system. However, due to its incompleteness, we still do not know if the implementation behavior matches the design behavior. In this paper, we provide a new solution for web applications. Since web application has special navigation character, we can get rich information in the log file after testing. From such log file, we extract the Petri net based behavior of the web application. The behavior is then checked by SPIN. Market Information System has been adopted as the case study.