Developing Reliable yet Flexible Software through If-Then Model Transformation Rules

Document Type : Research Article


1 Corresponding Author, A. Rasoolzadegan is with the department of Information Technology and Computer Engineering, Amirkabir University of Technology, Tehran, Iran (e-mail: rasoolzadegan,

2 A. Abdollahzadeh Barforoush is with the department of Information Technology and Computer Engineering, Amirkabir University of Technology, Tehran, Iran (e-mail:


Developing reliable yet flexible software is a hard problem. Although modeling methods enjoy a lot of advantages, the exclusive use of just one of them, in many cases, may not guarantee the development of reliable and flexible software. Formal modeling methods ensure reliability because they use a rigorous approach to software development. However, lack of knowledge and high cost practically force developers to use semi-formal methods instead. Semi-formal (visual) modeling methods, which are widely used in practical large-scale software development, are not good enough for reliable software development. This paper proposes a new approach to the development of reliable yet flexible software by transforming formal and semi-formal models into each other. In this way, the advantages of both methods are incorporated in to the software development process. The structured rules, proposed in this paper, transform formal and visual models into each other through the iterative and evolutionary process. The feasibility as well as the effectiveness of the proposed approach is demonstrated using the multi-lift system as a test case. 


[1] Y. Chen and H. Miao, “From an Abstract Object-Z Specification to UML Diagram,” Information & Computational Science, vol. 1 (2), pp. 319-324, 2004.
[2] D. Roe, K. Broda, and A. Russo, A. “Mapping UML models incorporating OCL constraints into object-z,” Tech. Rep., Dept. Computing, Imperial College London, 2003.
[3] S. Kim and D. Carrington, “A Formal Mapping between UML Models and Object-Z Specifications,” in Proc. Formal Specification and Development in Z and B, UK, Lecture Notes in Computer Science, vol. 1878, Springer, 2000.
[4] A. Rasoolzadegan and A. Abdollahzadeh, “Empirical Evaluation of Modeling Languages Using Multi-Lift System Case Study,” in Proc. 8th annual Int. Conf. on Modeling, Simulation and Visualization Methods, Nevada, USA, 2011.
[5] A. Rasoolzadegan and A. Abdollahzadeh. (2011). 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. [Online]. Available:
[6] A. Rasoolzadegan and A. Abdollahzadeh, “A New Approach to Reliable yet Flexible Software,” in Proc. 18th CAiSE Doctoral Consortium, London, United Kingdom.
[7] 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), Barcelona, Spain, 2011.
[8] R. N. Charette, “Why software fails,” IEEE Spectrum, vol. 42 (9), pp. 42-49, 2005.
[9] D. Bjørner, Software Engineering III: Domains, Requirements, and Software Design, Springer, 2006.
[10] J. R. Williams, “Automatic Formalization of UML to Z,” MSc. thesis, Dept. Computer Science, Univ. York, 2009.
[11] R. Pressman, Software Engineering: A Practitioner’s Approach, 7th ed., McGraw Hill, 2009.
[12] I. Somerville, Software Engineering, 8th ed., Addison Wesley, 2006.
[13] E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Pattern: Elements of Reusable Object-Oriented Software, Addison-Wesley Publishing Company, Fifth printing, 1995.
[14] J. Bowen, M. Hinchey, “Seven more myths of formal methods,” IEEE Software, vol. 12 (4), pp. 34–41, 1995.
[15] T. Tilley, “Formal Concept Analysis Applications To Requirements Engineering And Design,” Ph.D. dissertation, The Univ. Queensland, Australia, 2004.
[16] 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, vol. 2495 of LNCS, Springer, pp. 548-560, 2002.
[17] A. Evans, R. France, K. Lano, and B. Rumpe, “The UML as aformal modeling notation,” in Proc. UML'98: Beyond the Notation, France, vol. 1618 of LNCS, pp. 336-348, 1998.
[18] H. Miao, L. Liu, and L. Li, “Formalizing UML models with Object-Z,” in Proc. ICFEM2002: Conf. on Formal Eng. Methods, Springer-Verlag, pp. 523–534, 2002.
[19] D. Jackson, I. Schechter, and I. Shlyakhter, “Alcoa: the Alloy constraint analyzer,” in Proc. the International Conf. on Softw. Eng., Limerick, Ireland, pp. 730–733, 2000.
[20] J. Bowen. (2003). The world wide web virtual library: The Z notation. [Online]. Available:
[21] J. Sun, J. S. Dong, J. Liu, and H. Wang, “A formal object approach to the design of ZML,” Annals of Software Engineering, vol. 13, pp. 329–356, 2002.
[22] N. Plat, J. V. Karwijk, and K. Pronk, “A case for structured analysis/formal design,” in Proc. Formal Software Development Methods, vol. 552 of LNCS, pp: 81-105, 1991.
[23] J. Dick and J. Loubersac, “Integrating structured and formal methods: A visual approach to VDM,” in Proc. European Softw. Eng. Conf., vol. 550 of LNCS, pp. 37-59, 1991.
[24] F. Polack, “SAZ: SSADM version 4 and Z,” in Proc. Softw. Specification Methods: an overview using a case study, Springer, pp. 21-38, 2001.
[25] K. C. Mander, F. Polack, “Rigorous specification using structured systems analysis and Z,” Information and Software Technology, vol. 37 (5), pp. 285-291, 1995.
[26] N. Nagui-Raïss, “A formal software specification tool using the entity-relationship model,” in Proc. Entity-Relationship Approach, vol. 881 of LNCS, pp. 316-332, Springer, 1994.
[27] A. Galloway, “Integrated Formal Methods with Richer Methodological Profiles for the Development of Multi-Perspective Systems,” PhD thesis, Univ. Teesside, School of Computing and Mathematics, 1996.
[28] France, R.B. (1992) “Semantically extended data flow diagrams: A formal specification tool,” IEEE Trans. on Softw. Eng., vol. 18 (4), pp. 329-346.
[29] L. Semmens, R. B. France, and T. W. G. Docker, “Integrated structured analysis and formal specification techniques,” The Computer Journal, vol. 35 (6), 1992.
[30] A. Hall, “Using Z as a specification calculus for object-oriented systems,” in Proc. VDM '90, vol. 428 of LNCS, pp. 290-318, Springer, 1990.
[31] 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, Springer, pp. 307-326, 1996.
[32] R. B. France, M. M. Larrondo-Petrie, “An integrated object-oriented and formal model environment,” Journal of Object-Oriented Programming, vol. 10 (7), pp. 25-34, 1997.
[33] R. B. France, E. Grant, and J. M. Bruel, “UMLtranZ: A UML-based rigorous requirements modeling technique,” Tech. Rep., Colorado State Univ., 2000.
[34] 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 Softw. Technology, Berlin, vol. 1349 of LNCS, Springer, 1997.
[35] J. M. Bruel and R. B. France, “Transforming UML models to formal specifications,” in Proc. UML'98: Beyond the Notation, France, vol. 1618 of LNCS, Springer, 1998.
[36] E. Meyer and J. Souquiμeres, “Systematic approach to transform OMT diagrams to a B specification,” in Proc. FM'99, France, vol. 1708 of LNCS, pp. 875-895, 1999.
[37] 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, Springer, pp. 57-77, 2001.
[38] 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, Springer, 2001.
[39] 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, Grenoble, vol. 2272 of LNCS, Springer, pp. 517-534, 2002.
[40] H. Treharne, “Supplementing a UML development process with B,” in Proc. FME 2002: Formal Methods - Getting it Right, vol. 2391 of LNCS, Springer, pp. 568-586, 2002.
[41] A. Hammad, B. Tatibouët, 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, Springer, pp. 511-522, 2001.
[42] C. Snook and M. Butler, “UML-B: Formal modeling and design aided by UML,” ACM Trans. Softw. Eng. Methodol, vol. 15 (1), pp. 92-122, 2006.
[43] B. Selic and J. Rumbaugh, “Using UML for modeling complex real-time systems,” Tech. Rep., ObjecTime, 1998.
[44] 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, 2001.
[45] G. Engels, J. M. Küster, and R. Heckel, “A methodology for specifying and analyzing consistency of object-oriented behavioral models,” in Proc. 9th ACM SIGSOFT Symposium on Foundations of Softw. Eng., pp. 186-195, 2001.
[46] J. Davies and C. Crichton, “Concurrency and refinement in the UML,” in Proc. Refine 2002: the BCS FACS Refinement Workshop, vol. 70 (3) of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2002.
[47] J. Araújo, “Metamorphosis: An Integrated Object-Oriented Requirements Analysis and Specification Method,” PhD thesis, Dept. of Computing, Univ. Lancaster, 1996.
[48] K. Achatz and W. Schulte, “A formal OO method inspired by Fusion and Object-Z,” in Proc. ZUM'97: The Z Formal Specification Notation, vol. 1212 of LNCS, pp. 91-111, 1997.
[49] S. Dupuy, Y. Ledru, and M. Chabre-Peccoud, “Integrating OMT and Object-Z”, in Proc. of BCS FACS/EROS ROOM Workshop, 1997.
[50] 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, Grenoble, vol. 2272 of LNCS, Springer, pp. 497-516, 2002.
[51] F. Bouquet, F. Dadeau, and J. Groslambert, “Checking JML specifications with B machines,” in Proc. ZB 2005, vol. 3455 of LNCS, Springer, pp. 434-453, 2005.
[52] A. Eden, “Precise specification of design patterns and tool support in their application,” PhD thesis, Dept. Comp Science, Tel Aviv University, 2000.
[53] A. Eden, “Formal specification of object oriented design,” in Proc. Int. Conf. on Multidisciplinary Design in Engineering, CSME-MDE, 2001.
[54] R. Raje and S. Chinnasamy, “elelepus - a language for specification of software design patterns,” in Proc. ACM symposium on Applied computing, pp. 600-604, 2001.
[55] A. Flores, R. Moore, and L. Reynoso, “A formal model of object-oriented design and GoF design patterns,” in Proc. FME 2001: Int. Symposium of Formal Methods Europe, vol. 2021 of LNCS, pp. 223-241, Springer, 2001.
[56] L. Reynoso and R. Moore, “GoF behavioral patterns: a formal specification,” Tech. Rep., The United Nations Univ., 2000.
[57] S. Blazy, F. Gervais, and R. Laleau, “Reuse of specification patterns with the B method,” in Proc. ZB 2003: Formal Specification and Development in Z and B, Turku, Finland, vol. 2651 of LNCS, Springer, pp. 40-57, 2003.
[58] S. Kim and D. Carrington “A rigorous foundation for pattern-based design models,” in Proc. ZB 2005: Int. Conf. of B and Z users, vol. 3455 of LNCS, Springer, pp. 242-261, 2005.
[59] T. Taibi, Design Pattern Formalization Techniques, UAE, IGI Publishing, Hershey, New York, 2007.
[60] J. Kong, K. Zhang, J. Dong, and D. Xu, “Specifying behavioral semantics of UML diagrams through graph transformations,” The Journal of Systems and Softw., vol. 82, pp. 292-306, 2009.
[61] Y. Chen and H. Miao, “From an Abstract Object-Z Specification to UML Diagram,” Journal of Information & Computational Science, vol. 1 (2), pp.319-324, 2004.
[62] J. Sun, J. S. Dong, J. Liu, and H. Wang, “Object-Z web environment and projections to UML,” in Proc. 10th Int. WWW Conf., New York, ACM, pp. 725–734, 2001.