Which diagrams/aspects of UML are not formal and need an external formal technique/tool to analyse the associated produced model in UML? I mean external utilities which is not in the existing dominant UML CASE tools like Rational Rose.
The most obvious choice are Activity Diagrams. There is a formal semantics (which is a prerequisite to have a formal tool) for UML2.0 Activity Diagrams by Harald Störrle but I think it was not updated when UML evolved, since he is now working on other topics.
Rik Eshuis built a tool for a subset of UML1.5 Activity Diagrams. I think that an up-to-date, efficient tool for Activity Diagrams would be a strong contribution to the field.
Pierre: Thanks so much for the answer. Very good point. Do you think it would be feasible to transform an existing real world (big and complex) Activity Diagram and feed other Formal tools to verify/analyse that model? And if so would you suggest some existing Formal Tools for that?
Yes, it looks doable. You will have to decide which formal analyses you want to perform. Model-checking will probably require abstraction. If you have really huge AD you might want to resort to static analysis.