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.