Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2007)
Sept. 10, 2007 to Sept. 14, 2007
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2007.45
Krishna K. Mehra , Microsoft Research India
Sriram K. Rajamani , Microsoft Research India
A. Prasad Sistla , University of Illinois at Chicago
Sumit K. Jha , Carnegie Melon University
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.
A. P. Sistla, S. K. Jha, K. K. Mehra and S. K. Rajamani, "Verification of Object Relational Maps," 2007 IEEE International Conference on Software Engineering and Formal Methods(SEFM), London, 2007, pp. 283-292.