Can UML with OCL be used for formal specifications?

Hi mate,

I found an easy way to mix conditions and business rules with UML. I either add a note, constraint or condition to my diagram at graphical level directly inside the diagram or directly in the metamodel. I mean that if I add this constraints in the metamodel then this information is available directly in the model and live synchrnized with all graphical diagrams having this element. If I click on the diagram or select the element then I can see the constraint. This is the reuse of the same model element in more than one diagram. Very very impressive !!

Omondo EclipseUML has developped a new concept which allows to trace model element during all the development stages. They can trace at requirement, modeling and integration the same model element without transformation stages because they are live synchronized with MOF. It seems to be a crazy idea but when you use it it is really cool and very powerfull. This is a new concept and almost a hack therefore few documentations are available.

btw, I found this demo on the OCL and UML 2.2 (demo in French language 3mn):

Flash demo : http://www.download-omondo.com/regle_ocl.swf

.exe file for windows : http://www.download-omondo.com/regle_ocl.exe

Hope this help.

Thank you, although your answer starts with "Yes", the result seems to be "No":) Could you provide some example of semantic variation being useful? I mean, why not to fully formalize UML?

Gabriel Ščerbák 2010-05-12 09:35:38

Many people have tried to formalize the UML but all of them have failed (UML is too large and too complex). At most they have managed to formalize specific subsets by reexpressing UML in some formal language.

Jordi Cabot 2010-05-13 22:33:19

There is almost nothing concerning my question in your answer. It seems like you just wanted to advertise Omondo. I am not entirely sure what you mean by tracing, but there is a standard trace dependency in UML, which can be used to connect the same element in different contexts/development phases.

Gabriel Ščerbák 2010-05-12 09:32:59

I only like the tool :-)I don't mean to add dependencies which have trace stereotype I mean to have the same element using the same ID. You can create 100 diagrams and still just have one element because for Omondo each diagram is a view of the model and not the model itself.At implementation stage the Java Id is merge with the UML Id. It means that even at implementation stage you can trace your element created at model level. What is the most incredible is the merge. You can change your code manually and then just update the model and redo it again and again.Whaoo !!

2010-05-12 11:46:33

@roko-sifredi ah, the feature of separating model and diagrams is quite commong to good UML tools... I also saw the transformation traceability using IDs, but I am really not fond of reverese engineering in a way you described. Imagine you have domain model in your class diagram and you generate POJOs from it. Once you create an utility class, how omondo would know it is not an entity and should not be in the class diagram?

Gabriel Ščerbák 2010-05-13 08:15:53

EclipseUML can reverse java annotations into the model therefore @Entity is reversed.What I mean with model is to be on the top of the metamodel and not manipulate an internal model then transform it. Only Omondo provides this feature and no other tool in the world !!

2010-05-13 09:00:39

ansaurus

tags:

views:

answers:

Can UML with OCL be used for formal specifications?

related questions