An approach to detection of UML-based ownership violation

ABSTRACT

In this paper, we study how to detect the ownership violation based on the Unified Modeling Language (UML 2.0) in IBM Eclipse Modeling Framework. We develop a novel technique for automatically detecting the ownership violation in a program against its design class diagram using a software model checker. Specifically, given the fields that are intended to implement ownership in a UML class diagram, our approach checks the ownership property in two steps. First, the approach systematically generates all valid object diagrams, i.e. valid input program states. Then, after a method to destroy the owner object is called on each object diagram, the approach checks whether all external links to the owned objects have been removed. Central to this approach is how to prune away the large search space that includes all valid input program states.

REFERENCES

• 1: Object Management Group: Unified Modeling Language: Superstructure, version 2.0, August 2005.
• 2: D. Akehurst, G. Howells, K. McDonald-Maier: Implementing Associations: UML 2.0 to Java 5, In Software System Model, 6(2007), 3--35.
• 3: SAT4J Model Checker: http://www.sat4j.org.
• 4: Chandrasekhar Boyapati , Barbara Liskov , Liuba Shrira, Ownership types for object encapsulation, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-223, January 15-17, 2003, New Orleans, Louisiana, USA
• 5: Yann-Gaël Guéhéneuc , Hervé Albin-Amiot, Recovering binary class relationships: putting icing on the UML cake, Proceedings of the 19th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 24-28, 2004, Vancouver, BC, Canada
• 6: Ana Milanova, Precise identification of composition relationships for UML class diagrams, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1101922]
• 7: Daniel Jackson , Craig A. Damon, Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector, IEEE Transactions on Software Engineering, v.22 n.7, p.484-495, July 1996 [doi>10.1109/32.538605]
• 8: Joshua Bloch, Effective java™, second edition, Prentice Hall Press, Upper Saddle River, NJ, 2008
• 9: Frank Budinsky , Stephen A. Brodsky , Ed Merks, Eclipse Modeling Framework, Pearson Education, 2003
• 10: Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , Helmut Veith, Modular verification of software components in C, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 11: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]

INDEX TERMS

Keywords:
Eclipse, UML, class diagram, model checker, ownership