A Library-Based Approach to Translating OCL Constraints to JML Assertions for Runtime Checking

OCL is a formal notation to specify constraints on UML models that cannot otherwise be expressed by diagrammatic notations such as class diagrams. Using OCL one can document detailed design decisions and choices along with the behavior, e.g., class invariants and method pre and post-conditions. However, OCL constraints cannot be directly executed and checked at run-time by an implementation, thus constraint violations may not be detected or noticed, causing many potential development and maintenance problems. In this paper, the authors propose an approach to checking OCL constraints at run-time by translating them to executable JML assertions. The key components of their approach are a set of JML library classes, use of model variables, and a separation of JML assertions from source code.