Integrating UML and Formal Methods

• DOI: 10.1016/j.entcs.2007.03.017
• Publication Date: 2007-06-30T07:20:29Z
• Authors: Rafael Magalhães ...; Alexandre Cabral ...
• Keywords: OhCircus; formal methods; 0202 electrical engineering, electronic engineering, information engineering; translation; refinement; 02 engineering and technology; UML; Theoretical Computer Science; Computer Science(all)

AbstractUML is a widespread language used in both industry and academia, despite the fact that its semantics is still informal and allows ambiguities. On the other hand, OhCircus is a formal specification language which unifies Z, CSP, the refinement calculus of Morgan and object-oriented theories. In this work we integrate UML class diagrams and OhCircus by written UML elements in terms of OhCircus constructs. However, instead of a simply syntactical mapping, we also propose the concept of a class model to capture associations and global constraints. Finally, we use this integration to prove the refinement of associations as attributes, a result that relates analysis to design to implementation and which is very common in industry.