Using UML and Maude for writing and reasoning about ODP policies

We present a graphical UML-based notation for writing ODP actions and policies, which can be directly mapped to Maude specifications. Our approach may introduce important benefits to the (usually ambiguous) UML specifications, such as formal support, provision for rigorous specifications, and easy access to Maude´s toolkit. We have developed a tool for automating the translation process and for giving access to Maude´s analysis tools. In this way we try to bridge the current gap between graphical and formal notations, by providing an easy-to-use environment for modeling enterprise business systems with UML, but still with formal support.