Bidirectional Transformation of Structural Modeling Elements between the UML Class Diagram and Object-Z
Subject Areas : electrical and computer engineering
A.
Rasoolzadegan
1
Ahmad
Abdollahzadeh Barforoush
2
(Amirkabir)
Keywords: Model transformation the UML class diagram Object-Z the multi-lift system,
Abstract :
In this paper, a new mechanism is proposed to transform the structural modeling elements of the UML class diagram and Object-Z specifications into each other. A set of bidirectional rules is defined to transform the mentioned elements into each other. Bidirectional transformation of the UML class diagram, as one of the most useful diagrams of UML, and Object-Z specifications into each other prepares the ground for the use of the unique advantages of both formal and visual modeling methods. The feasibility of the proposed approach is evaluated using the multi-lift case study. The results of conducting the multi-lift case study show that the proposed mechanism is feasible.
[1] D. C. Schmidt, "Model-driven engineering," IEEE Computer, vol. 39, no. 2, pp. 25-31, Feb. 2006.
[2] Q. Charatan and A. Kans, Formal Software Development: from VDM to Java, Palgrave Macmillan, 2004.
[3] D. Bjorner, Software Engineering III: Domains, Requirements, and Software Design, Springer, 2006.
[4] J. R. Williams, Automatic Formalization of UML to Z, MSc. Thesis, Dept. Computer Science, Univ. York, 2009.
[5] A. Hall, "Seven myths of formal methods," IEEE Software, vol. 7, no. 5, pp. 11-19, Sep. 1990.
[6] J. Bowen and M. Hinchey, "Seven more myths of formal methods," IEEE Software, vol. 12, no. 4, pp. 34-41, Jul. 1995.
[7] D. Bojic and D. Velasevic, "Reverse engineering of use case realizations in UML," in Proc. Symp. on Applied Computing - SAC2000, ACM, vol. 2, pp. 741-747, 2000.
[8] A. Rasoolzadegan and A. Abdollahzadeh, "A new approach to software development process with formal modeling of behavior based on visualization," in Proc. 6th Int. Conf. on Softw. Eng. Advances, ICSEA, pp. 104-111, Barcelona, Spain, 2011.
[9] A. Rasoolzadegan and A. Abdollahzadeh, Specifying a Parallel, Distributed, Real-Time, and Embedded System: Multi-Lift System Case Study, Tech. Rep., Information Technology and Computer Eng. Faculty, Amirkabir Univ. Technology, Tehran, Iran, 2011.
[10] J. Kong, K. Zhang, J. Dong, and D. Xu, "Specifying behavioral semantics of UML diagrams through graph transformations," The J. of Systems and Software, vol. 82, no. 2, pp. 292-306, Apr. 2009.
[11] R. Duke and G. Rose, Formal Object - Oriented Specification Using Object - Z, MacMillan Press, 2000.
[12] E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Pattern: Elements of Reusable Object - Oriented Software, Addison - Wesley Publishing Company, 5th Ed., 1995.
[13] T. Tilley, Formal Concept Analysis Applications to Requirements Engineering and Design, Ph. D. Dissertation, the Univ. Queensland, Australia, 2004.
[14] J. Sun, J. S. Dong, J. Liu, and H. Wang, "Object - Z web environment and projections to UML," in Proc. 10th Int. World Wide Web Conf., New York, ACM, pp. 725-734, 2001.
[15] J. Bowen (2003) frequently asked questions, [Online], Available: http://www.faqs.org/faqs/z-faq.
[16] J. Bowen (2003) The World Wide Web virtual library: The Z notation, Available: http://www.zuser.org/z.
[17] J. Sun, J. S. Dong, J. Liu, and H. Wang, "A formal object approach to the design of ZML," Annals of Software Engineering: an International J., vol. 13, no. 14, pp. 329-356, 2002.
[18] Extensible Markup Language-XML (2003) World Wide Web Consortium, Available: http://www.w3.org/XML.
[19] S. K. Kim and D. Carrington, "Visualization of formal specifications," in Proc. 6th Asia - Pacific Softw. Eng. Conf., pp. 38-45, Dec. 1999.
[20] S. K. Kim and D. Carrington, "Formalizing the UML class diagram using Object - Z," in Proc. the Second IEEE Conf. on UML, UML'99, pp. 83-98, 1999.
[21] S. K. Kim and D. Carrington, "An integrated framework with UML and Object - Z for developing a precise and understandable specification: the light control case study," in Proc. Seventh Asia - Pacific Software Engineering Conf., pp. 240-248, 2000.
[22] S. Kim and D. Carrington, "A formal meta - modeling approach to a transformation between the UML state machine and Object-Z," in Proc. ICFEM 2002: Int. Conf. Formal Eng. Methods, pp. 548-560, Shanghai, China, 2002.
[23] E. Wafula and P. Swatman, "FOOM: a diagrammatic illustration of inter-object communication in Object-Z specifications," in Proc. the Asia-Pacific Software Engineering Conf., APSEC'95, 23 pp., 1995.
[24] S. German, "Research goals for formal methods," ACM Computing Surveys, vol. 28, no. 4es, p. 118. 1996.
[25] E. Borger, "High level system design using abstract state machines," in Proc. Current Trends in Applied Formal Methods (FM - Trends 98), Springer LNCS 1641, pp. 1-43, 1998.
[26] E. Clarke and J. Wing, "Formal methods: state of the art and future directions," ACM Computing Surveys, vol. 28, no. 4, pp. 626-643, Dec. 1996.
[27] A. Evans, R. France, K. Lano, and B. Rumpe, "The UML as a formal modeling notation," in Proc. UML'98: Beyond the Notation, vol. 1618 of LNCS, Springer, pp. 336-348, Mulhouse, France, 1998.
[28] H. Miao, L. Liu, and L. Li, "Formalizing UML models with Object-Z," in Proc. ICFEM2002: Conf. on Formal Eng. Methods, pp. 523-534, 2002.
[29] D. Jackson, "A comparison of object modeling notations: alloy, UML and Z," unpublished manuscript, [Online], Available: http://sdg.lcs.mit.edu/˜dnj/pubs/alloy-comparison.pdf, 1999.
[30] D. Jackson, I. Schechter, and I. Shlyakhter, "Alcoa: the alloy constraint analyzer," in Proc. of the Int. Conf. on Software Engineering, pp. 730-733, Limerick, Ireland, 2000.
[31] D. Jackson, Software Abstractions: Logic, Language, and Analysis, MIT Press, 2006.
[32] S. Agerholm and P. Larsen, "A lightweight approach to formal methods," in Proc. the Int. Workshop on Current Trends in Applied Formal Methods, pp. 168-183, 1998.
[33] P. G. Larsen, J. V. Katwijk, N. Plat, K. Pronk, and H. Toetenel, "SVDM: an integrated combination of SA and VDM," in Proc. Methods Integration Workshop, 1991.
[34] N. Plat, J. V. Karwijk, and K. Pronk, "A case for structured analysis/formal design," in Proc. Formal Software Development Methods, VDM'91, vol. 552 of LNCS, pp. 81-105, 1991.
[35] M. D. Fraser, K. Kumar, and V. K. Vaishnavi, "Informal and formal requirements specification languages: bridging the gap," IEEE Trans. on Softw. Eng., vol. 17, no. 5, pp. 454-465, May 1991.
[36] J. Dick and J. Loubersac, "Integrating structured and formal methods: a visual approach to VDM," in Proc. ESEC'91: European Softw. Eng. Conf., vol. 550 of LNCS, pp. 37-59, Milan, Italy, 1991.
[37] V. Hamilton, "Experience of combining Yourdon and VDM," in Proc. the Methods Integration Workshop, pp. 529-555, 1991.
[38] L. T. Semmens and P. Allen, "Using Yourdon and Z: an approach to formal specification," in Proc. Fifth Annual Z User Meeting, Oxford, Springer, pp. 228-253, 1991.
[39] F. Polack, M. Whiston, and K. C. Mander, "The SAZ project: integrating SSADM and Z," in Proc. FME'93: Industrial-Strength Formal Methods, vol. 670 of LNCS, pp. 541-557, 1993.
[40] F. Polack, "SAZ: SSADM version 4 and Z," in Proc. Software Specification Methods: An Overview Using a Case Study, pp. 21-38, 21-38, London, UK, 2001.
[41] K. C. Mander and F. Polack, "Rigorous specification using structured systems analysis and Z," Information and Software Technology, vol. 37, no. 5, pp. 285-291, 1995.
[42] N. Nagui - Raiss, "A formal software specification tool using the entity - relationship model," in Proc. ER'94: Entity - Relationship Approach, vol. 881 of LNCS, pp. 316-332, 1994.
[43] A. Galloway, Integrated Formal Methods with Richer Methodological Profiles for the Development of Multi - Perspective Systems, Ph. D Thesis, University of Teesside, School of Computing and Mathematics, 1996.
[44] R. B. France, "Semantically extended data flow diagrams: a formal specification tool," IEEE Trans. on Softw. Eng., vol. 18, no. 4, pp. 329-346, Apr. 1992.
[45] L. T. Semmens, R. B. France, and T. W. G. Docker, "Integrated structured analysis and formal specification techniques," The Computer Journal, vol. 35, no. 6, pp. 600-610, 1992.
[46] D. Harel, "Statecharts: a visual formalism for complex systems," Science of Computer Programming, vol. 8, no. 3, pp. 231-274, 1987.
[47] A. Hall, "Using Z as a specification calculus for object - oriented systems," in Proc. VDM'90, vol. 428 of LNCS, pp. 290-318, Dublin, Ireland, 1990.
[48] A. Hall, "Specifying and interpreting class hierarchies in Z," in Proc. Z User Workshop, Cambridge, Workshops in Computing, pp. 120-138, 1994.
[49] J. Hammond, "Producing Z specifications from object - oriented analysis," in Proc. Z User Workshop, Cambridge, Workshops in Computing, Springer, pp. 316-336, 1994.
[50] M. Rawson and P. Allen, "Synthesis: an integrated, object - oriented method and tool for requirements specification," in Proc. Method Integration Workshop, Leeds, UK, Electronic Workshops in Computing (eWIC), 320-334, Leeds, UK, 1996.
[51] M. Weber, "Combining statecharts and Z for the design of safety - critical control systems," in Proc. FME'96: 3rd Int. Symposium of Formal Methods Europe, vol. 1051 of LNCS, pp. 307-326, Oxford, UK, 1996.
[52] R. B. France, J. M. Bruel, and G. Raghavan, "Towards rigorous analysis of fusion models: the MIRG experience," in Proc. 2nd Northern Formal methods Workshop, Electronic Workshops in Computing, British Computer Society, 280-289, Ilkley, UK, 1996.
[53] R. B. France and M. M. Larrondo - Petrie, "An integrated object -oriented and formal model environment," J. of Object-Oriented Programming, vol. 10, no. 7, pp. 25-34, 1997.
[54] R. B. France, E. Grant, and J. M. Bruel, UMLtranZ: An UML - Based Rigorous Requirements Modeling Technique, Tech. Rep., Colorado State University, 2000.
[55] R. B. France, J. M. Bruel, M. M. Larrondo - Petrie, and E. Grant, "Rigorous object - oriented modeling: integrating formal and informal notations," in Proc. Algebraic Methodology and Software Technology, AMAST'97, vol. 1349 of LNCS, pp. 216-230, Munich, Germany, 1997.
[56] J. M. Bruel and R. B. France, "Transforming UML models to formal specifications," in Proc. UML'98: Beyond the Notation, vol. 1618 of LNCS, Springer, pp. 165-18, Mulhouse, France, 1998.
[57] S. Dupuy, Couplage de Notations Semi - Formelles et Formelles Pour la Specification des Systemes D'information, Ph.D. Thesis, Universite Joseph Fourier, Grenoble I, 2000.
[58] K. Lano and H. Haughton, "Improving the process of system specification and development in B," in Proc. 6th Refinement Workshop, Workshops in Computing, pp. 42-56, Oxford, UK, 1994.
[59] K. Lano, H. Haughton, and P. Wheeler, "Integrating formal and structured methods in object - oriented system development," Formal Methods and Object Technology, pp.113-157, 1996.
[60] P. Facon, R. Laleau, and H. P. Nguyen, "Mapping object diagrams into B specifications," in Proc. Method Integration Workshop, UK, Electronic Workshops in Computing (eWIC), pp. 1-13, 1996.
[61] A. Malioukov, "An object - based approach to the B formal method," in Proc. B'98: Int. B Conf., vol. 1393 of LNCS, pp. 162-181, Montpellier, France, 1998.
[62] H. Nguyen, Derivation De Specifications Formelles B a partir de Specifications Semi-Formelles, Ph.D. Thesis, Laboratoire CEDRIC, Conservatoire National des Arts et Metiers, Evry, France, 1998.
[63] E. Meyer and J. Souquiµeres, "Systematic approach to transform OMT diagrams to a B specification," in Proc. FM'99, vol. 1708 and 1709 of LNCS, pp. 875-895, Toulouse, France, 1999.
[64] C. Snook and M. Butler, Tool - supported use of UML for constructing B specifications, [Online], Available: http://www.ecs.soton.ac.uk/~mjb/, 2000.
[65] P. Facon, R. Laleau, and H. P. Nguyen, "From OMT diagrams to B specifications," in Proc. Softw. Spec. Methods: an Overview Using a Case Study, pp. 57-77, Potsdam, German, 2001.
[66] R. Laleau and F. Polack, "A rigorous metamodel for UML static conceptual modeling of information systems," in Proc. CAiSE 2001: Advanced Information Systems Eng., vol. 2068 of LNCS, pp. 402-416, Interlaken, Switzerland, 2001.
[67] R. Laleau and F. Polack, "Specification of integrity - preserving operations in information systems by using a formal UML - based language," Information and Software Technology, vol. 43, no. 12, pp. 693-704, 2001.
[68] R. Laleau and F. Polack, "Coming and going from UML to B: a proposal to support traceability in rigorous IS development," in Proc. ZB 2002: Formal Specification and Development in Z and B, vol. 2272 of LNCS, pp. 517-534, Grenoble, France, 2002.
[69] H. Treharne, "Supplementing a UML development process with B," in Proc. FME 2002: Formal Methods-Getting it Right, vol. 2391 of LNCS, pp. 568-586, Copenhagen, Denmark, 2002.
[70] A. Hammad, B. Tatibouet, J. Voisinet, and W. Weiping, "From B specification to UML statechart diagrams," in Proc. ICFEM 2002: Int. Conf. of Formal Engineering Methods, vol. 2495 of LNCS, pp. 511-522, Shanghai, China, 2001.
[71] C. Snook and M. Butler, "UML - B: formal modeling and design aided by UML," ACM Trans. Softw. Eng. Methodol, vol. 15, no. 1, pp. 92-122, 2006.
[72] B. Selic and J. Rumbaugh, "Using UML for modeling complex real - time systems," in Proc. the ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems, LCTES'98), pp. 250-260, Montreal, Canada, 1998.
[73] C. Fischer, E. Olderog, and H. Wehrheim, "A CSP view on UML - RT structure diagrams," in Proc. Fundamental Approaches to Softw. Eng., vol. 2029 of LNCS, Springer, pp. 91-108, Genova, Italy, 2001.
[74] G. Engels, J. M. Kuster, and R. Heckel, "A methodology for specifying and analyzing consistency of object - oriented behavioral models," in Proc. 9th ACM SIGSOFT Symp. on Foundations of Softw. Eng., pp. 186-195, Vienna, Austria, 2001.
[75] J. Davies and C. Crichton, "Concurrency and refinement in the UML," in Proc. Refine 2002: the BCS FACS Refinement Workshop, Electronic Notes in Theoretical Computer Science, vol. 70, no. 3, pp. 217-243, Nov. 2002.
[76] J. Araujo, Metamorphosis: an Integrated Object-Oriented Requirements Analysis and Specification Method, Ph.D. Thesis, Dept. of Computing, University of Lancaster, 1996.
[77] K. Achatz and W. Schulte, "A formal object-oriented method inspired by fusion and Object - Z," in Proc. ZUM'97: the Z Formal Specification Notation, Int. Conf., vol. 1212 of LNCS, pp. 91-111, Reading, UK, 1997.
[78] S. Dupuy, Y. Ledru, and M. Chabre-Peccoud, "Integrating OMT and Object-Z," in Proc. BCS FACS/EROS ROOM Workshop, pp. 347-366, London, UK, 1997.
[79] S. Kim and D. Carrington, "A formal mapping between UML models and Object - Z specifications," in Proc. ZB2000: Formal Specification and Development in Z and B, York, UK, Lecture Notes in Computer Science, vol. 1878, pp. pp. 2-21, York, UK, 2000.
[80] S. Kim and D. Carrington, "A formal model of the UML meta - model: the UML state machine and its integrity constraints," in Proc. ZB 2002, vol. 2272 of LNC, pp. 497-516, Grenoble, France, 2002.
[81] F. Bouquet, F. Dadeau, and J. Groslambert, "Checking JML specifications with B machines," in Proc. ZB 2005, vol. 3455 of LNCS, pp. 434-453, Guildford, UK, 2005.
[82] Y. Chen and H. Miao, "From an abstract Object - Z specification to UML diagram," J. of Information & Computational Science, vol. 1, no. 2, pp.319-324, 2004.