Model checking database applications. We describe the design of DPF, an explicit-state model checker for database-backed web applications. DPF interposes between the program and the database layer, and precisely tracks the effects of queries made to the database. We experimentally explore several implementation choices for the model checker: stateful vs. stateless search, state storage and backtracking strategies, and dynamic partial-order reduction. In particular, we define independence relations at different granularity levels of the database (at the database, relation, record, attribute, or cell level), and show the effectiveness of dynamic partial-order reduction based on these relations.par We apply DPF to look for atomicity violations in web applications. Web applications maintain shared state in databases, and typically there are relatively few database accesses for each request. This implies concurrent interactions are limited to relatively few and well-defined points, enabling our model checker to scale. We explore the performance implications of various design choices and demonstrate the effectiveness of DPF on a set of Java benchmarks. Our model checker was able to find new concurrency bugs in two open-source web applications, including in a standard example distributed with the Spring framework.
References in zbMATH (referenced in 3 articles , 1 standard article )
Showing results 1 to 3 of 3.
- Bozzelli, Laura; Molinari, Alberto; Montanari, Angelo; Peron, Adriano: Model checking interval temporal logics with regular expressions (2020)
- Bozzelli, Laura; Molinari, Alberto; Montanari, Angelo; Peron, Adriano; Sala, Pietro: Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy (2018)
- Gligoric, Milos; Majumdar, Rupak: Model checking database applications (2013)