A verifier for interactive, data-driven web applications

摘要

We present WAVE, a verifier for interactive, database-driven Web applications specified using high-level modeling tools such as WebML. WAVE is complete for a broad class of applications and temporal properties. For other applications, WAVE can be used as an incomplete verifier, as commonly done in software verification. Our experiments on four representative data-driven applications and a battery of common properties yielded surprisingly good verification times, on the order of seconds. This suggests that interactive applications controlled by database queries may be unusually well suited to automatic verification. They also show that the coupling of model checking with database optimization techniques used in the implementation of WAVE can be extremely effective. This is significant both to the database area and to automatic verification in general.