View all Seminars  |  Download ICal for this event

Modeling and verification of database-accessing applications

Series: M.Tech (Research) Colloquium

Speaker: Geetam Chawla

Date/Time: Jun 21 12:00:00

Location: Online

Faculty Advisor: Komondoor V. Raghavan

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 languages, 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 testing 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, analysis 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. The tool was evaluated on a set of 58 specifications. The tool found 35 of these to be satisfied; of the rest, upon manual analysis, we found that two were genuinely violated, while the remaining 21 "unsatisfied" warnings were actually false positives. This preliminary evaluation reveals that the approach is scalable and quite precise.
Teams meeting link:

Speaker Bio:

Host Faculty: Komondoor V. Raghavan