Verification of Object Relational Maps

Enterprise software systems need to deal with two dominant data models. While object oriented languages (such as Java, C#, C++) are the dominant ways to write business logic, relational databases are the dominant ways to store data. Object-relational (OR) maps are widely used to mediate between thes...

Full description

Saved in:
Bibliographic Details
Main Authors: Mehra, K.K., Rajamani, S.K., Jha, S.K., Sistla, A.P.
Format: Conference Proceeding
Language:English
Subjects:
Algebra
Application software
Automatic testing
Data models
Formal verification
Java
Logic
Object oriented databases
Object oriented modeling
Relational databases
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Enterprise software systems need to deal with two dominant data models. While object oriented languages (such as Java, C#, C++) are the dominant ways to write business logic, relational databases are the dominant ways to store data. Object-relational (OR) maps are widely used to mediate between these two data models. We present a system to verify correctness of OR maps. We formulate simple correctness conditions for OR maps, and convert these conditions to validity of formulas in first order logic. We have built a verification tool called ROUND TRIP that is able to both validate and find errors in OR maps defined in the ESQL language of the Microsoft EDM data model.
ISSN:1551-0255
2160-7656
DOI:10.1109/SEFM.2007.45