Seminars

Automatic Data Generation for Web Application Validation PDF slides
Shoichiro Fujiwara,
Fujitsu Laboratories

10/25/10, 2 PM, GHC-6501

Abstract

The talk begins with a description of SWEEP, a validation tool for server-side Java applications using application frameworks. SWEEP is constructed on top of Java PathFinder (JPF), a program model checker for Java. The tool includes a frontend driver, a framework stub and a database stub. To validate a web application with SWEEP, we first describe business specifications formally. The formal specification is used as properties to be checked. Then we generate application data for a frontend driver and a database stub from the specifications. By populating the data, SWEEP drives the application exhaustively to check the specifications.

After describing SWEEP, I describe the details of data generation. Data generation is one of the key technologies in SWEEP. It decides the reachability of program execution path at the state which satisfies the pre-condition to be checked. The inputs to the data generation tool are business specifications, a database schema, and predicates like cardinality and foreign key relations. The data generation tool packages the inputs into a constraint solved by a Satisfiability Modulo Theories (SMT) solver. The solution is then used to generate input driver/database stub data for the web application.

Biography

Shoichiro Fujiwara is a research staff member of software innovation laboratories in Fujitsu Laboratories, Kawasaki (Japan). Before joining Fujitsu in 2007, he earned a B.A. in engineering (2005) and an M.A. in informatics (2007) from Kyoto University. His research interests are formal methods, decision procedures, SMT solvers, and web/enterprise software verification