Abstract
The process of validating a web application with respect to its business specification is manually intensive. This often results in having to deploy a system in the field without adequate testing leading to costly failures. In this talk I will present our work in automating validation of enterprise web applications.

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.

BIO
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.