Dresden OCL Logo
Dresden OCL
OCL support for your modeling language

Contents

Success Stories

Dresden OCL has been integrated into various tools and has been used in various research projects. The list below summarises some of these success stories of Dresden OCL.

Integrations

CASE Tools

ArgoUML

The Dresden OCL Toolkit has been integrated into the open-source CASE tool ArgoUML.

Fujaba4Eclipse

The Fujaba Tool Suite is developed at the university of Paderborn. One project based on the Fujaba Tool Suite is Fujaba4Eclipse. Fujaba4Eclipse is as an open source project and its goal is to provide an integrated teaching environment based on Eclipse for secondary schools and first year university courses. It should assist teaching object-oriented technology, design patterns and the syntax and semantics of a programming language.

In 2005 and 2006 Mirko Stölzel integrated parts of the Dresden OCL2 Toolkit into Fujaba4Eclipse (for his student research projects Großer Beleg and Diploma Thesis), to use OCL constraints in class and story diagrams created with Fujaba4Eclipse.

MagicDraw™

MagicDraw™ is a business process, architecture, software and system modeling tool with teamwork support. MagicDraws OCL2 evaluation implementation is based on the Dresden OCL2 Toolkit. MagicDraw uses a modified version of the toolkit which has reduced size and has been adapted to the MagicDraw repository.

More information about MagicDraw is available at http://www.magicdraw.com/.

MetaBoss

MetaBoss, a dually licensed Model-Driven-Architecture toolkit makes use of the Dresden OCL Toolkit for modelling of service specifications and domain entities. It also allows generation of validation code from the OCL in a model.

Poseidon

Poseidon is the commercial successor of ArgoUML and also contains the integration of the Dresden OCL Toolkit just as its predecessor does.

Other Tools

HOL-OCL

HOL-OCL is an interactive proof environment for the Object Constraint Language (OCL). It is implemented as a shallow embedding of OCL into the Higher-order Logic (HOL) instance of the interactive theorem prover Isabelle. HOL-OCL is developed by Achim D. Brucker and Burkhart Wolff.

HOL-OCL defines a machine-checked formalization of the semantics as described in the standard for OCL 2.0. This conservative, shallow embedding of UML/OCL into Isabelle/HOL includes support for typed, extensible UML data models supporting inheritance and subtyping inside the typed λ-calculus with parametric polymorphism. As a consequence of conservativity with respect to higher-order logic (HOL), we can guarantee the consistency of the semantic model. Moreover, HOL-OCL provides several derived calculi for UML/OCL that allows for formal derivations establishing the validity of UML/OCL formulae. Automated support for such proofs is also provided.

HOL-OCL uses the Dresden OCL Toolkit as repository and the OCL2-Parser for type checking.

More information in: http://www.brucker.ch/projects/hol-ocl/index.de.html.

Incremental OCL

Incremental OCL is a prototype tool that assist you in the efficient implementation of OCL constraints in any final technology-platform.

It gives you information about the kind of changes over the system state that can violate a constraint, the instances must be verified after each change and possible redefinitions of the original constraint that result in a better efficiency of the integrity checking process.

The tool is implemented as a set of Java classes extended with the libraries of the Dresden OCL toolkit (for parsing and loading the OCL ICs) and NetBeans MDR (for the import/export from XMI files).

More information in: http://www.lsi.upc.edu/~jcabot/research/IncrementalOCL/.

KIEL

KIEL (Kiel Integrated Environment for Layout) presents an alternative paradigm for visualizing Statecharts during simulation. OCL and the Dresden OCL Toolkit is used to handle well-formedness rules for UML state machines.

More information available at http://rtsys.informatik.uni-kiel.de/~rt-kiel/.

Documentation available at http://infoscience.epfl.ch/record/97176/files/ProchnowSBvH06.pdf, http://rtsys.informatik.uni-kiel.de/~biblio/downloads/talks/martes06-talk.pdf and http://rtsys.informatik.uni-kiel.de/~biblio/downloads/theses/kbe-dt.pdf.

OCL Transformation Tool

Due to the high expressiveness of the OCL, the designer has different syntactic alternatives to express each constraint. This tool assists the designer during the definition of the constraints by means of generating equivalent alternatives for the initially defined ones.

In the context of the MDA, transformations between these different alternatives are required as part of the PIM-to-PIM, PIM-to-PSM or PIM-to-code transformations of the original conceptual schema.

Specially, the OCL Transformation Tool is able to generate all alternative equivalent representations of a constraint obtained by means of changing the context type used to define the original constraint.

The OCL Transformation Tool uses the Dresden OCL Toolkit to parse constraints for which the tool generates all possible context changes.

More information at: http://www.lsi.upc.edu/~jcabot/research/OCLTransformations/.

UMLtoCSP

UMLtoCSP is a tool for the formal verification of UML/OCL models using Constraint Programming. It can check automatically several correctness properties about the model, such as the satisfiability of the model or the lack of contradictory constraints.

UMLtoCSP uses the Dresden OCL Toolkit to parse and load OCL constraints.

More information at: http://gres.uoc.edu/UMLtoCSP/.

XText-OCL2Java Validator

The XText-OCL2Java Validator was developed by a student (Jan Löbel) at the University of Applied Science in Furtwangen in 2011. The tool can be used to extend XText with validation support for OCL rules. Dresden OCL's OCL2AspectJ code generator was modified to generated plain Java code that is afterwards registered as a Java validator within the XText parser of the constrained language.

More information can be found at http://code.google.com/p/xtext-ocl2javavalidator/

Nomos Software's XML Validation Service

Nomos Software provides an online service to validate XML SEPA messages againts their XML Schema as well as additional well-formedness-rules implemented in OCL. The evaluation of these OCL rules has been implemented by applying the OCL2Java code generator of a former Dresden OCL release. Besides, Nomos also uses MagicDraw for OCL validation (which as well integrated Dresden OCL as discussed above). Further information on their use cases and MagicDraw can be found at [1] and [2].

Experimental or Legacy Integrations

Borland Together

Dresden OCL Toolkit 1.3 has been prototypically integrated into Borland Together.

Rational Rose

An integration into Rational Rose has been performed. This integration package is not in the public domain, however.

Projects

Entre2Mers

Entre2Mers was a project of the Electricite de France (EDF). In a EDF data warehouse, many historical databases should be reconstituted. This issue raises database quality problems of different categories like different name and addresses of the same person in different databases. In order to gain more confidence in information contained in relational databases, a database quality analysis tool was developed.

After experiments with an own language, OCL was used to express the constraints. In order to implement it, the OCL2SQL module was integrated into the EDF database quality tool.

Ericsson

In Telecommunication system, network devices process huge amount of data supplied by the network operators. It is crucial for the devices to obtain approved data which adheres to certain pre defined restrictions to avoid failures during later stages. Therefore, the data sent by the network operator has to be validated against large number of constraints before it is processed by the network devices. Even though operators are aware of these constraints, but the inherent ambiguity associated with the natural language specification of constraint makes it difficult to send the correct data. The Object Constraint Language (OCL) can play a vital role in specifying these constraints in an unambiguous manner. Ericsson, a Telecommunication giant aims to use OCL not only for constraint specification but also for automation of code generation from the OCL constraints. The use of OCL in Ericsson’s systems and the feasibility of code generation from these constraints was investigated by two students of the Märladarlen University, Sweden in 2010 (Master thesis task description).

After the evaluation of the existing open source OCL tools, Dresden OCL was selected for customization as per Ericsson’s requirement. The domain-specific models of Erricson were adapted to the pivot model of Dresden OCL. Furthermore, the code generator and the code generation templates of OCL2Java/AspectJ were customized to generate Java code rather than aspect code from the constraints.

Priyadarshan Patil--one of the implementors--reports: OCL is integral part of modeling which helps to make the models complete and helps to move towards Model Driven Development. Modeling is given lot of emphasis in Ericsson systems. Our work in the field of OCL has impressed everyone in Ericsson and has fetched us several accolades. This includes Best innovative idea implementation award at an Ericsson internal IBM conference. Our work in field of OCL has raised interest of other Ericsson subsystems who are inspired to use the same in their projects.

JEFF

JEFF is a framework for building business applications developed by sd&m. OCL was used to specify constraints (both invariants and pre and post conditions) on JEFF classes and components. Although the complexity of such specifications can grow very rapidly, it is possible that a (right) use of OCL can increase the quality of code and the performance of the software development process. Note that the JEFF specification is based on OCL 2.0 and thus could not yet be checked with Dresden OCL Toolkit modules.

KeY Project

The aim of the KeY Project is to integrate formal software specification and verification into the industrial software engineering processes. The starting point is a commercial CASE tool, which is augmented by capabilities for formal specification and verification. The ultimate goal is to make the verification process transparent for the user with respect to the informal object-oriented model.

KeY uses a modified version of the OCL Parser which is part of the Dresden OCL Toolkit.

nxCom

nxCom is a commercial product providing a business directory service. During the development of the nxCom business logic module the OCL2Java and the OCLInjector4Java tool were tested (see Ralf Wiebicke's diploma thesis for more information). The nxCom module was instrumented with Java code that checks invariants (mainly business rules) against test data. Many constraint violations could be detected in that way.

Spatial OCL

Cemagref (Agricultural and environmental engineering research) develops environmental and agricultural databases. That way the institute implemented a checking mechanism for spatial constraints based on a specific extension of the OCL2SQL module ("Spatial OCL"). This extension has been used to produce automatically Oracle Spatial SQL queries from spatial constraints. Several queries have been generated and have been used to check the consistency of an agricultural database for organic sewage management.