Modeling and verification of database-accessing applications

Abstract

Databases are central to the functioning of most IT-enabled processes and services. In many domains, databases are accessed and updated via applications written in general-purpose lan- guages, as such applications need to contain the business logic and workflows that are key to the organization. Therefore, automated tools are required not only for creation and test- ing of database schemas and queries, etc., but also for analysis, testing, and verification of database-accessing applications. In this work we describe a novel approach for modeling, anal- ysis and verification of database-accessing applications. We target applications that use Object Relational Mapping (ORM), which is the common database-access paradigm in most Model- View Controller (MVC) based application development frameworks. In contrast with other approaches that try to directly analyze and prove properties of complex database accessing ORM-based code, our approach infers a relational algebra specification of each controller in the application. This specification can then be fed into any off-the-shelf relational algebra solver to check properties (or assertions) given by a developer. We have implemented this approach as a tool that works for ‘Spring’ based MVC applications. A preliminary evaluation reveals that the approach is scalable and quite precise.