Abstract
The Model Driven Architecture (MDA) involves automated trans-formations between software models defined in different languages at different abstraction levels. This paper takes an MDA approach to integrate a formal modeling language (Object-Z) with an informal modeling language (UML) via model transformation. This paper shows how formal and informal modeling languages can be cooperatively used in the MDA framework and how the trans-formations between models in these languages can be achieved using an MDA development environment. The MDA model transformation techniques allow us to have a reusable transformation between formal and informal modeling languages. The integrated approach provides an effective V&V technique for the MDA.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Dascalu, S., Hitchcock, P.: An approach to integrating semi-formal and formal notations in software specification. ACM symposium on Applied computing, 1014–1020 (2002)
DSTC, Tefkat: The EMF transformation engine, http://www.dstc.edu.au/Research/Projects/Pegamento/tefkat/index.html
DSTC Transformation Language, MOF query/views/ transformations: Second revised sub-mission (2004), http://www.omg.org/docs/ad/04-01-06.pdf
Duke, R., Rose, G.: Formal Object-Oriented Specification Using Object-Z. Macmillan, Basingstoke (2000)
Eclipse Foundation, http://www.eclipse.org/
EclipseUML, Omondo, http://www.eclipsedownload.com/
EMF, The eclipse modeling framework, http://download.eclipse.org/tools/emf/scripts/docs.php?doc=references/overview/EMF.html
France, R., Wu, J., Larrondo-Petrie, M.M., Bruel, J.-M.: A Tale of Two Case Studies: Using Integrated Methods to Support Rigorous Requirements Specification. In: Proc. BCS FACS Methods Integration Workshop 1996 (1996)
Kim, S.-K., Carrington, D.: A Formal Mapping between UML Models and Object-Z Specifications. In: P. Bowen, J., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, pp. 2–21. Springer, Heidelberg (2000)
Kim, S.-K.: A Metamodel-based Approach to Integrate Object-Oriented Graphical and Formal Specification Techniques, PhD Thesis, ITEE, The University of Queensland (2002)
Laleau, R., Polack, F.: Coming and going from UML to B: A proposal to support traceability in rigorous IS development. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 517–534. Springer, Heidelberg (2002)
Lano, K., Clark, D., Androutsopoulos, K.: UML to B: Formal Verification of Object-Oriented Models. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 187–206. Springer, Heidelberg (2004)
Lilius, J., Paltor, I.P.: Formalizing UML state machines for model checking. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 430–445. Springer, Heidelberg (1999)
McUmber, W., Cheng, B.: A General Framework for Formalizing UML with Formal Languages. In: IEEE Conference on Software Engineering, pp. 433–442 (2001)
Ng, M.Y., Butler, M.: Tool Support for Visualizing CSP in UML. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 287–298. Springer, Heidelberg (2002)
OMG, Meta Object Facility (MOF),1.4, OMG Document ad/02-04-03 (2002)
OMG, MOF 2.0 Query/Views/Transformations RFP, OMG Document ad/02-04-10 (2002)
OMG, MDA Guide Version 1.0.1(2003), http://www.omg.org/docs/omg/03-06-01.pdf
OMG, UML 2.0 Superstructure Specification, OMG Document ptc/03-08-02 (2003), http://www.omg.org/docs/ptc/03-08-02.pdf
Sendall, S., Kozaczynski, W.: Model Transformation: The Heart and Soul of Model-Driven Software Development. IEEE Software, 42–45 (September/October 2003)
Sun, J., Dong, J.S., Liu, J., Wang, H.: Z family on the web with their UML photos, http://nt-appn.comp.nus.edu.sg/fm/zml/
UML2, The eclipse UML2 project, http://www.eclipse.org/uml2/
Wieringa, R., Dubois, E., Huyts, S.: Integrating Semi-formal and Formal Requirements. In: Olivé, À., Pastor, J.A. (eds.) CAiSE 1997. LNCS, vol. 1250, pp. 19–32. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kim, SK., Burger, D., Carrington, D. (2005). An MDA Approach Towards Integrating Formal and Informal Modeling Languages. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_30
Download citation
DOI: https://doi.org/10.1007/11526841_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27882-5
Online ISBN: 978-3-540-31714-2
eBook Packages: Computer ScienceComputer Science (R0)