%0 Journal Article %1 borges_07_integrating %A Borges, Rafael M. %A Mota, Alexandre C. %B Proceedings of the Second Brazilian Symposium on Formal Methods (SBMF 2005) %D 2007 %J Electronic Notes in Theoretical Computer Science %K 2007 formal_methods uml %P 97--112 %R 10.1016/j.entcs.2007.03.017 %T Integrating UML and Formal Methods %U http://dx.doi.org/10.1016/j.entcs.2007.03.017 %V 184 %X UML 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.

@article{borges_07_integrating, abstract = {UML 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.}, added-at = {2009-02-11T20:48:19.000+0100}, author = {Borges, Rafael M. and Mota, Alexandre C.}, biburl = {https://www.bibsonomy.org/bibtex/219117e5413c058c19023b8d3f498c274/leonardo}, booktitle = {Proceedings of the Second Brazilian Symposium on Formal Methods (SBMF 2005)}, citeulike-article-id = {1685821}, doi = {10.1016/j.entcs.2007.03.017}, interhash = {44584e91c586eb7ba185c04a20acb99b}, intrahash = {19117e5413c058c19023b8d3f498c274}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {2007 formal_methods uml}, month = {July}, pages = {97--112}, posted-at = {2007-11-29 12:07:21}, priority = {3}, timestamp = {2009-02-11T20:48:19.000+0100}, title = {Integrating UML and Formal Methods}, url = {http://dx.doi.org/10.1016/j.entcs.2007.03.017}, volume = 184, year = 2007 }