This Article 
 Bibliographic References 
 Add to: 
Formalizing and Integrating the Dynamic Model for Object-Oriented Modeling
August 2002 (vol. 28 no. 8)
pp. 747-762

Abstract—The Object Modeling Technique (OMT), a commonly used object-oriented development technique, comprises the object, dynamic, and functional models to provide three complementary views that graphically describe different aspects of systems. The lack of a well-defined semantics for the integration of the three models hinders the overall development process, particularly during the design phase. Previously, we formalized the object model in terms of algebraic specifications. However, the algebraic specifications only capture the static, structural aspects of a system. They do not explicitly describe the behavior, which is critical for system development especially for the design phase. It is necessary to formalize the dynamic model in terms of the structural descriptions in order to specify and verify the system behavior using rigorous techniques. This paper presents a well-defined formal model for both the object and dynamic models and their integration. The formal model is described in terms of a well-known specification language, LOTOS. Formalization of the graphical notation enables numerous automated processing and analysis tasks, such as behavior simulation and consistency checks between levels of specifications.

[1] D. Craigen, S. Gerhart, and T. Ralston, “Formal Methods Reality Check: Industrial Usage,” IEEE Trans. Software Eng., vol. 21, no. 2, pp. 90–98, Feb. 1995.
[2] J.M. Wing, “A Specifier's Introduction to Formal Methods,” IEEE Computer, vol. 23, pp. 8–24, Sept. 1990.
[3] J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, and W. Lorensen, Object-Oriented Modeling and Design. Englewood Cliffs, N.J.: Prentice Hall, 1991.
[4] D. Harel, “Statecharts: A Visual Formalism for Complex Systems,” Science of Computer Programming, vol. 8, pp. 231–274, July 1987.
[5] T. Bolognesi and E. Brinksma, “Introduction to the ISO Specification Language LOTOS,” The Formal Description Technique LOTOS, P.H.J.V. Eijk, C.A. Vissers, and M. Diaz, eds., pp. 23–73, 1989.
[6] E.Y. Wang and B.H.C. Cheng, “Formalizing the Functional Model Within Object-Oriented Design,” Int'l J. Software Eng. and Knowledge Eng., vol. 10, no. 1, pp. 5–30, 2000.
[7] E.Y. Wang and B.H.C. Cheng, “A Rigorous Object-Oriented Design Process,” Proc. Int'l Conf. Software Process, June 1998.
[8] A. Azcorra, J. Quemada, and J. Manas, “LOTOS Tool Survey,” Sept. 1992.
[9] R.H. Bourdeau and B.H.C. Cheng, “A Formal Semantics of Object Models,” IEEE Trans. Software Eng., vol. 21, pp. 799–821, Oct. 1995.
[10] B.H.C. Cheng, E.Y. Wang, and R.H. Bourdeau, “A Graphical Environment for Formally Developing Object-Oriented Software,” Proc. IEEE Sixth Int'l Conf. Tools with Artificial Intelligence, Nov. 1994.
[11] H. Ehrig and B. Mahr, Fundamentals of Algebraic Specification. Berlin: Springer-Verlag, 1985.
[12] E.Y. Wang and B.H. Cheng, “An Application of a Rigorous Design Process,” Technical Report MSU-CPS-98-6, Dept. of Computer Science, Michigan State Univ., East Lansing, Feb. 1998.
[13] B.H.C. Cheng, L.A. Campbell, and E.Y. Wang, “Enabling Automated Analysis Through the Formalization of Object-Oriented Diagrams,” Proc. IEEE Int'l Conf. Dependable Systems and Networks (FTCS-30 and DCCA-8), pp. 305–314, June 2000.
[14] J.L. Sharnowski, G.C. Gannod, and B.H. Cheng, “A Distributed Multimedia Environmental Information System,” Proc. IEEE Int'l Conf. Multimedia and Computing Systems, pp. 142–194, May 1995.
[15] R.H. Bourdeau, B.H.C. Cheng, and B. Pijanowski, “A Regional Information System for Environmental Data Analysis,” Photogrammetric Eng.&Remote Sensing, vol. 62, pp. 855–861, July 1994.
[16] J.V. Guttag, J.J. Horning, K.J.S.J. Garland, A. Modet, and J. Wing, Larch: Languages and Tools for Formal Specification, Texts and Monographs in Computer Science, Springer-Verlag, 1993.
[17] D. Harel, A. Pneuli, J.P. Schmidt, and R. Sherman, “On the Formal Semantics of Statecharts,” Proc. Second IEEE Symp. Logic in Computer Science, pp. 54–64, 1987.
[18] D. Latella, I. Majzik, and M. Massink, “Towards a Formal Operational Semantics of UML Statechart Diagrams,” Proc. Third Int'l Conf. Formal Methods for Open Object-Based Distributed Systems, Feb. 1999.
[19] “BetterState,” , 1997.
[20] P. vanEijk, “Tools for LOTOS Specification Style Transformation,” Formal Description Techniques, II, S. Vuong, ed., pp. 43–51, 1990.
[21] J.A. Manas, T. de Miguel, J. Salvachua, and A. Azcorra, “Tool Support to Implement LOTOS Formal Specifications,” Computer Networks and ISDN Systems, vol. 25, pp. 815–839, 1993.
[22] L. Andriantsiferana, B. Ghribi, and L. Logrippo, “Prototyping and Formal Requirement Validation of GPRS: A Mobile Data Packet Radio Service for GSM,” Proc. Seventh Int'l Working Conf. Dependable Computing For Critical Applications (DCCA-7), pp. 99–118, Jan. 1999.
[23] Q. Fu, P. Harnois, L. Logrippo, and J. Sincennes, “Feature Interaction Detection: A Lotos-Based Approach,” Computer Networks, pp. 433–448, 2000.
[24] N.C. Levenson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese, "Requirements Specification for Process-Control Systems," IEEE Trans. Software Eng., vol. 20, no. 9, pp. 684-707, Sept. 1994.
[25] J. Rumbaugh, I. Jacobson, and G. Booch, The Unified Modeling Language Reference Manual. Addison Wesley, 1999.
[26] C.A. Vissers, G. Scollo, M. vanSinderen, and E. Brinksma, “Specification Styles in Distributed Systems Design and Verification,” Theoretical Computer Science, vol. 89, no. 1, pp. 179–206, 1991.
[27] J.Q. Vives, S.P. Gomez, and D.L. Lopez, “LOLA: Quick Reference version 3R6,” technical report, Univ. Politécnica de Madrid, Oct. 1994.
[28] A.M.D. Moreira and R.G. Clark, “Adding Rigour to Object-Oriented Analysis,” Software Eng. J., vol. 11, no. 5, pp. 270–280, 1996.
[29] R. Jungclaus, G. Saake, T. Hartmann, and C. Sernadas, “TROLL—A Language for Object-Oriented Specification of Information Systems,” ACM Trans. Information Systems, 1996.
[30] B. Selic, G. Gullekson, and P. T. Ward, Real-Time Object-Oriented Modeling. New York: Wiley&Sons, 1994.
[31] M. Shroff and R.B. France, “Towards a Formalization of UML Class Structures in Z,” Proc. 21st Ann. Int'l Computer Software and Applications Conf. (COMPSAC '97), pp. 646–651, Aug. 1997.
[32] J. Lilius and I.P. Paltor, “The Semantics of UML State Machines,” Proc. UML '99 conf., Oct. 1999.
[33] P. Bose, “Automated Translation of UML Models of Architecture for Verification and Simulation Using SPIN,” Proc. IEEE Int'l Conf. Automated Software Eng., Oct. 1999.
[34] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[35] W.M. Ho, J.-M. Jezequel, A.L. Guennec, and F. Pennaneach, “UMLAUT: An Extendible UML Transformation Framework,” Proc. IEEE Int'l Conf. Automated Software Eng., Oct. 1999.
[36] W.E. McUmber and B.H. Cheng, “UML-Based Analysis of Embedded Systems Using a Mapping to VHDL,” Proc. IEEE High Assurance Software Eng. (HASE '99), Nov. 1999.
[37] W.E. McUmber and B.H.C. Cheng, “A General Framework for Formalizing UML with Formal Languages,” Proc. IEEE Int'l Conf. Software Eng. (ICSE '01), May 2001.
[38] L.A. Campbell and B.H.C. Cheng, “Object-Oriented Modeling and Automated Analysis of a Telemedicine Application,” Proc. IEEE Int'l Workshop Software Specification and Design (IWSSD-10), Nov. 2000.

Index Terms:
Object-oriented modeling, formal specification, behavior, dynamic model, requirements analysis, design, model integration.
Betty H.C. Cheng, Enoch Y. Wang, "Formalizing and Integrating the Dynamic Model for Object-Oriented Modeling," IEEE Transactions on Software Engineering, vol. 28, no. 8, pp. 747-762, Aug. 2002, doi:10.1109/TSE.2002.1027798
Usage of this product signifies your acceptance of the Terms of Use.