Automated Model-basedAnalysisOfWeb-basedUserInterface(UI)
Stc
Date: 2009-02-05
Time: 11:45
Room: BBL room 471
Speaker: Xiaoyu Cui
Title: Automated Model-based analysis of Web-based User Interface(UI) (thesis defense)
Abstract
Many companies have moved to use web applications to run their business (interact with their customers, internal administrations, business scheduling, etc) and to provide global access over Internet to their business. Web-based User interface (Web-based UI) allows a user to interact with a web application. It is usually the only entry point for users to the web application, hence its good design is crucial to the web application’s availability.
In the normal Web-based UI development lifecycle, there are some manual works required for evaluating the specification against Web-based UI designs and implementations. With the rapid growth in number and complexity of web applications, those manual works are error-prone and time-consumed; we would need a tool to avoid those manual works.
In this thesis, we introduce a framework which can carry out Model-based analysis to avoid such manual works. We propose an extension to Kripke structure[1] which is more suitable to model web-based UIs and shows how to represent UI specifications in CTL[2]. We also propose a scheme to translate our UI models and its CTL specifications to the input language of the model checker SMV so that we can do verification (on the models). Furthermore, we propose a scheme to automatically generate tests from UI models. Unlike the model checking approach, the tests are to be exercised on the real UI. We extend an existing tool called selenium[3] to invoke test cases to collect all information from real UIs. Based on those information, we compose another UI model which reflects the real UI and using SMV model checker to verify the CTL specifications.
[1]. E. A. Emerson E. M. Clarke and A. P. Sistla. Automatic verification of finite-state concurrent
systems using temporal logic specifications. ACM Transactions on Programming Languages
and Systems, 1986.
[2]. P. Schnoebelen. The complexity of temporal logic model checking. Advances in Modal Logic,
4:393–436, 2003.
[3]. Jason Huggins C. Titus Brown, Gheorghe Gheorghiu. An introduction to testing web applications with twill and selenium. O’Reilly Media.
