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.
%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
}