Verification of Object-Relational Maps
- Krishna Mehra ,
- Prasad Sistla ,
- Sriram Rajamani ,
- Sumit K. Jha
Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM) |
Published by IEEE Computer Society
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 ROUNDTRIP that is able to both validate and find errors in OR maps defined in the ESQL language of the Microsoft EDM data model.
Copyright © 2007 IEEE. Reprinted from IEEE Computer Society. This material is posted here with permission of the IEEE. Internal or personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution must be obtained from the IEEE by writing to pubs-permissions@ieee.org. By choosing to view this document, you agree to all provisions of the copyright laws protecting it.