Nowadays many software applications are deployed over compute clouds using the three-tier architecture, where the persistent data for the application is stored in a backend datastore and is accessed and modified by the server-side code based on the user interactions at the client-side. The data model forms the foundation of these three tiers, and identifies the set of objects stored by the application and the relations (associations) among them. In this dissertation, we present automated techniques for data model specification, verification and repair.

We first present an approach for automated verification of data models that 1) extracts a formal data model from an object-relational mapping, 2) converts verification queries about the data model to queries about the satisfiability of logic formulas, and 3) uses an automated decision procedure to check the satisfiability of the resulting formulas. To improve the ease-of-use for this formal verification framework, we provide property templates for specifying data model properties, which are automatically translated to logical formulas before verification.

To further automate the specification and verification process, we present techniques for automatically inferring properties about the data model by analyzing the relations among the object classes, and identifying patterns that correspond to a subset of our property templates. We then check the inferred properties on the data model using our automated verification techniques. For the properties that fail, we present techniques that generate fixes to the data model that establish the inferred properties.

We implemented these techniques in a tool for analyzing web applications built using the Ruby on Rails framework and applied it to five open source applications. Our experimental results demonstrate that our approach is effective in automatically identifying and fixing errors in data models of real-world web applications.