Model Checking Large Complex Web Applications
Sree Rajan ( Fujitsu Labs )
- 11:00 19th February 2010 ( week 5, Hilary Term 2010 )278
Web applications are released to customers in Beta mode due to tremendous pressure on time-to-market. In order to check end-to-end functional behavior of web applications, conventional testing tools have not matched extremely short release cycles.
Formal verification tools such as model checkers and light-weight theorem provers have tried to evolve from small-scale research prototypes to efficient dependable work horses.
However, they are still largely percieved as lagging behind conventional testing with respect to usability and scalability, and rightly-so.
In this talk we present the design and architecture of a tool called Web Applications Validation Environment (WEAVE) centered around model checking and symbolic execution for finding bugs in web applications implemented using multiple programming/scripting languages.
In the first part of this talk, we'll discuss the following aspects of WEAVE related to the server-portion of a web application:
(1) an intuitive interface for developers to construct requirements that are compiled into temporal logic to address the issue of usability, (2) a semi-automatic method for environment generation to constrain the behavior of a (web) client-server application for model checking and (3) symbolic execution tailored to finding functional and security bugs.
We have successfully applied WEAVE to detect bugs in several large Web applications upto a million lines of code.
In the second part, we'll discuss our approach to the challenges posed by the client portion of a web application such as
(1) Javascript and flash (2)Mapping Ajax web page changes to client state changes (3) Avoiding recrawling the entitre web application to regenerate the state model.
In the last part of the talk we'll outline our efforts on deploying verification tools on the cloud, making them available as a service to product groups within Fujitsu.
Formal verification tools such as model checkers and light-weight theorem provers have tried to evolve from small-scale research prototypes to efficient dependable work horses.
However, they are still largely percieved as lagging behind conventional testing with respect to usability and scalability, and rightly-so.
In this talk we present the design and architecture of a tool called Web Applications Validation Environment (WEAVE) centered around model checking and symbolic execution for finding bugs in web applications implemented using multiple programming/scripting languages.
In the first part of this talk, we'll discuss the following aspects of WEAVE related to the server-portion of a web application:
(1) an intuitive interface for developers to construct requirements that are compiled into temporal logic to address the issue of usability, (2) a semi-automatic method for environment generation to constrain the behavior of a (web) client-server application for model checking and (3) symbolic execution tailored to finding functional and security bugs.
We have successfully applied WEAVE to detect bugs in several large Web applications upto a million lines of code.
In the second part, we'll discuss our approach to the challenges posed by the client portion of a web application such as
(1) Javascript and flash (2)Mapping Ajax web page changes to client state changes (3) Avoiding recrawling the entitre web application to regenerate the state model.
In the last part of the talk we'll outline our efforts on deploying verification tools on the cloud, making them available as a service to product groups within Fujitsu.
Speaker bio
Dr. Sree Rajan is a senior researcher at Fujitsu Laboratories of America leading a research program in dependable systems and cloud computing. He joined Fujitsu Laboratories from SRI International Computer Science Laboratory in 1996. His recent research has focused on developing scalable formal techniques to improve trust and security in web applications and cloud computing platforms. Besides his main responsibilities at Fujitsu, he serves as the founding Editor-in-Chief of ACM Transactions on Storage.Share this:
