Model-based testing of thin-client web applications and navigation input

More and more software systems use a browser as the universal graphical user interface. As a consequence these applications inherit browser navigation as part of their interface. Typical browser actions are the use of the back- and forward-button and the cloning of windows. Browser navigation is difficult to deal with because it has effects that are noticed indirectly by the application logic. It is easy to forget or misunderstand the consequences of this aspect in the construction of a program. Hence, testing the correct behavior of the application is very desirable, preferably with an automatic model-based test tool. For this kind of model-based testing a specification including browser navigation is needed. We introduce a transformation to lift the specification of a program without browser navigation to one with browser navigation. This reduces the specification effort considerably. The distinguishing feature of our method is that it allows the test engineer to specify only the exceptions to the general rule. We show how this lifting of specifications is used for some examples and how errors are found in real web applications. The described system builds on the model-based test tool GVST.