Validating OCL Specifications with the USE Tool—An Example Based on the BART Case Study

Abstract The Object Constraint Language (OCL) is part of the Unified Modeling Language (UML). Within software engineering, UML is regarded today as an important step towards development of high-quality object-oriented systems. OCL allows to sharpen UML diagrams through invariants as well as pre- and postconditions. This paper explains the functionality of the UML Specification Environment USE which allows to validate UML and OCL descriptions. The paper shows that central safety properties of the train system described in the well-known BART case study can be expressed with OCL. Test cases embodying central aspects of this train system can be formulated within the USE system. It can be shown that the safety properties are satisfied by the test cases examined.