Yes, I agree UML specifications are not precise and accurate.

I was thinking about it as a research assignment for one of my students, that can be extended to a master thesis. But now we have some other more concrete and interesting research directions. Lets see.

We are working on a project trying to integrate formal verification into a model-based development process, which use a subset of UML models + MARTE profile, to analyse some nonfunctional properties, e.g. response time. I think it is feasible.

The main difficulties of such work come from double sides. One is from UML. As you said, UML models are not precise, or too flexible, I would like to say. It is impossible to analyse an arbitrary UML model using formal verification, so we need to limit the elements of models. Then the question is what to choose. A small subset may make the formal verification easier, but at the same time it makes the models express only some very restrict applications therefore not really useful for real project. A large subset is good for project modeling however is difficult or impossible for formal verification.

Another difficulty is about how to choose proper formal verification techniques for a specific property.

Actually, a tool for validating OCL (and UML) specifications exists: The USE tool has been developed by Gogolla and Richters at the Universität Bremen in Germany. You can download it from http://sourceforge.net/projects/useocl/.

If you google "use ocl bremen" you will find a number of papers describing the theoretical background and a number of case studies.

I worked on this topic for my PhD thesis. In my case the focus was translating UML models into temporal logic. Depending on the formalism you choose and on the UML set you wan't to tackle the problem can get really difficult. Here you can find an updated list of what I worked on http://www.informatik.uni-trier.de/~ley/pers/hd/m/Motta:Alfredo.html

Hope it helps

It is definitively possible, there is a large number of researches around this topic, even more, the OMG has an attempt to standardize the basis for this integration, fUML. In this specification, there is a section called base semantics, which is a declarative semantics for fUML using first-order logic.

Note I did not answer yes for feasibility (considering available tools).

Maybe you can find some useful information in the following paper: “Using the Base Semantics given by fUML for Verification” including a brief review of the related works around this topic.

There are many approaches in this field, cf. e.g. http://www.sse-tubs.de/~rumpe/publications/papers/EFLR98d/EFLR98d.html and later research of Bernhard Rumpe.

I think, it's feasible, but you'll not have The Semantics, you can just gave A formalisation which is more suitable for your domain.

check out our tool for direct UML verification without any translations to any other formal languages.

We are releasing the new version soon.

here is the link http://www.comp.nus.edu.sg/~lius87/UMLSM.html

It depends on what you want to validate precisely, UML consistency (e.g. adhere to the OMG rules) or also the content or domain what is modeled in UML.

We are working on two types of tools in health care informatics / standards that take the following base approach: to model the domain UML is too a specific. So we created a profile for each project (they differ but can be linked on different levels of the health ICT architecture).

Based on the profile a set of rules can be determined for e.g. content. One example requires each data element to be a separate class. Hence that is a rule and that can be validated. Each class must have a semantic binding to unique code from a medical terminology. If that is not there the UML tool shows an ?, and the validation rules - once run through the validator - points the developer to missing code binding.

This data element tool has the validation in Microsoft .Net programmed (C#) against the UML tool (in our case Enterprise Architect from Sparx).

The second tool deals with functions and criteria for electronic health records. The specifications are all in UML packages and a UML class model profile is checking internal consistency of the model. Again the content is validated as well based on rules. The content validation is done externally. This time we export the UML model content in XML format (using a specific XML publication format called MAX). The MAX export is saved as file and an XML schema validation and schematron validation check if the MAX output adheres to the validation rules. The validation report is in XML and imported back into Enterprise Architect and shown to the user.

By the way, your question triggered excellent responses and a lot of useful tools I want to check further. Thank you all.

I agree with most of the answers that have been given so far about feasibility of integration.

You may be interested in checking a plugin we developed for integrating formal verification in the Topcased modeling environment. The modeling language is SysML, a UML.based language commonly used for industrial projects, and the application domain is safety-critical embedded automotive systems. You can find more information in this paper: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6059147

Hi,

my experience with searching for model checking tools for UML diagrams is that there are a lot of research tools around but none of them where completed to such an extend that they can be used off the shelf in an industrial project. Usability is usually not a requirement for research tools but it is definitely a requrement if you want to convince a project team to use a tool.

Currently we use COSIDE from Fraunhofer, which is a front end that translates UML statechart diagrams to NuSMV. The UML input language is restricted but I think that makes it easier to understand.

Karin

To be able to integrate Formal verification tools with UML we first need a common and consistent semantics for the different languages and notations that conform the unified modelling language. There is a very interesting paper in this direction by María Victoria Cengarle, Alexander Knapp, Andrzej Tarlecki and Martin Wirsing called "A Heterogeneous Approach to UML Semantics" (http://dl.acm.org/citation.cfm?id=1424949). Later, it is possible to design formal verification tools acting on descriptions obtained as translations of the original diagrams to this common language.

Carlos

Hi

this research is a new approach

there are many ways for translating UML models to Formal Specification.

you can convert the xmi format of UML model; so translate it to SMV or SPIN codes

for verifying specifications such as LTL and CTL