Abstract
We present a model of object-oriented and component-based refinement. For object-orientation, the model is class-based and refinement is about correct changes in the structure, methods of classes and the main program, rather than changes in the behaviour of individual objects. This allows us to prove refinement laws for both high level design patterns and low level refactoring. For component-based development, we focus on the separation of concerns of interface and functional contracts, leaving refinement of interaction protocols in future work. The model supports the specification of these aspects at different levels of abstractions and their consistency.
Based on the semantics, we also provide a general definitional approach to defining different relational semantic models with different features and constraints.
This is a revised and extended version of the combination of the papers [17,31]. This work is partly supported by e-Macao project funded by the Government of Macao, and the research grant 02104 MoE and the 973 project 2002CB312000 of MoST of P.R. China.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Cardeli, L.: A Theory of Objects. Springer, Heidelberg (1996)
Allen, R., Garlan, D.: A formal basis for architectural connection. ACM Transactions on Software Engineering and Methodology 6(3) (1997)
Arbab, F.: Reo: A channel-based coordination of model for component composition. Mathematical Structures in Computer Science 14(3), 329–366 (2004)
Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modelling Language User Guide. Addison-Wesley, Reading (1999)
Borba, P., Sampaio, A., Cornélio, M.: A refinment algebra for object-oriented programming. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, pp. 457–482. Springer, Heidelberg (2003)
Broy, M.: Object-oriented programming and software development - a critical assessment. In: McIver, A., Morgan, C. (eds.) Programming Methodology. Springer, Heidelberg (2003)
Broy, M., Stolen, K.: Specification and Development of Interactive Systems: FOCUS on Streams, Interfaces, and Refinement. Springer, Heidelberg (2001)
Cavalcanti, A., Naumann, D.A.: A weakest precondition semantics for an object-oriented language of refinement. Technical Report CS Report 9903, Stevens Institute of Technology, Hoboken, NJ 07030 (February 2000)
Cheesman, J., Daniels, J.: UML Components. Component Software Series. Addison-Wesley, Reading (2001)
Chen, Y., Sanders, J.W.: The weakest specifunction. Acta Informatica 41(7) (2005)
Filipe, J.K.: A logic-based formalization for component specification. Journal of Object Technology 1(3), 231–248 (2002)
Fowler, M.: What is the point of the UML. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003. LNCS, vol. 2863, pp. 325–325. Springer, Heidelberg (2003)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns, Elements of Reusable Object-Oriented Software. Addlison Wesley, Reading (1995)
Goessler, G., Sifakis, J.: Composition for component-based modeling. Science of Computer Programming
Hall, J.A.: Seven myths of formal methods. IEEE Software 7(5), 11–19 (1990)
He, J., Liu, Z., Li, X.: rCOS: A refinement calculus for object systems. Technical Report 322, UNU/IIST, P.O. Box 3058, Macao SAR China (2005)
He, J., Liu, Z., Li, X., Qin, S.: A relational model of object oriented programs. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 415–436. Springer, Heidelberg (2004)
Heineman, G.T., Councill, W.T.: Component-Based Software Engineering, Putting the Pieces Together. Addison-Wesley, Reading (2001)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)
Jacobson, I., Booch, G., Rumbaugh, J.: The Unified Software Development Process. Addison-Wesley, Reading (1999)
Jin, N., He, J.: Resource models and pre-compiler specification for hardware/software. In: Cuellar, J.R., Liu, Z. (eds.) Proc. 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), Beijing, China, September 28-30, 2004. IEEE Computer Society Press, Los Alamitos (2004)
Jones, C.B.: Process algebra arguments about an object-oriented design notation. In: Roscoe, A.W. (ed.) A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice Hall, Englewood Cliffs (1994)
Jones, C.B.: Accommodating interference in the formal design of concurrent object-based programs. Formal Methods in System Design 8(2), 105–122 (1996)
Kruchten, P.: The Rational Unified Process – An Introduction, 2nd edn. Addison-Wesly, Reading (2000)
Larman, C.: Applying UML and Patterns. Prentice Hall, Englewood Cliffs (2001)
Li, X., Liu, Z., He, J.: Formal and use-case driven requirement analysis in UML. In: COMPSAC 2001, Illinois, USA, October 2001, pp. 215–224. IEEE Computer Society Press, Los Alamitos (2001)
Li, X., Liu, Z., He, J., Long, Q.: Generating prototypes from a UML model of requirements. In: Ghosh, R.K., Mohanty, H. (eds.) ICDCIT 2004. LNCS, vol. 3347, pp. 255–265. Springer, Heidelberg (2004)
Liu, J., Liu, Z., He, J., Li, X.: Linking UML models of design and requirement. In: Proceedings of ASWEC 2004, Melbourne, Australia, pp. 329–338. IEEE Computer Society Press, Los Alamitos (2004)
Liu, Z.: Object-oriented software development in UML. Technical Report UNU/IIST Report No. 228, UNU/IIST, P.O. Box 3058, Macau, SAR, P.R. China (March 2001)
Liu, Z., He, J., Li, X.: Contract-oriented component software development. Technical Report UNU/IIST, Report No 298 (2004), http://www.iist.unu.edu/newrh/III/1/page.html
Liu, Z., He, J., Li, X.: Contract-oriented development of component systems. In: Proceedings of IFIP WCC-TCS 2004, Toulouse, France, pp. 349–366. Kluwer Academic Publishers, Dordrecht (2004)
Liu, Z., He, J., Li, X., Chen, Y.: A relational model for formal requirements analysis in UML. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 641–664. Springer, Heidelberg (2003)
Liu, Z., He, J., Li, X., Liu, J.: Unifying views of UML. Electronic Notes of Theoretical Computer Science (ENTCS) 101, 95–127 (2004)
Long, Q., He, J., Liu, Z.: Refactoring and pattern-directed refactoring: A formal perspective. Technical Report 318, UNU-IIST, P.O.Box 3058, Macau (January 2005)
Long, Q., Liu, Z., Li, X., He, J.: Consistent code generation from UML models. In: Pro. of Australian Software Engineering Conference (ASWEC 2005), Brisbane, Australia, pp. 168–177. IEEE Computer Society Press, Los Alamitos (2005)
Long, Q., Qiu, Z., Liu, Z., Shao, L., He, J.: POST: A case study for rcos incremental development. Technical Report 324, UNU/IIST, P.O. Box 3058, Macao SAR China (2005)
Mellor, S.J., Balcer, M.J.: Executable UML: a foundation for model-driven architecture. Addison-Wesley, Reading (2002)
Meyer, B.: From structured programming to object-oriented design: the road to Eiffel. Structured Programming 10(1), 19–39 (1989)
Meyer, B.: Applying design by contract. IEEE Computer (May 1992)
Meyer, B.: Object-oriented Software Construction, 2nd edn. Prentice Hall PTR, Englewood Cliffs (1997)
Pierik, C., de Boer, F.S.: A syntax-directed hoare logic for object-oriented programming concepts. Technical Report UU-CS-2003-010, Institute of Information and Computing Science, Utrecht University (2003)
Selic, B.: Using UML for modelling complex real-time systems. In: Müller, F., Bestavros, A. (eds.) LCTES 1998. LNCS, vol. 1474, pp. 250–262. Springer, Heidelberg (1998)
Sherif, A., Jifeng, H., Cavalcanti, A., Sampaio, A.: A framework for specification and validation of real-time systems using circus actions. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 478–494. Springer, Heidelberg (2005)
Smyth, M.: Powerdomain. Journal of Computer Science and System Sciences 16, 23–36 (1978)
Szyperski, C.: Component Software: Beyond Object-Oriented Programming. Addison-Wesley, Reading (2002)
Wing, J.M.: A specifier’s introduction to formal methods. IEEE Computer 23(9), 8–24 (1990)
Yang, J., Long, Q., Liu, Z., Li, X.: A predicative semantic model for integrating UML models. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 170–186. Springer, Heidelberg (2005)
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
Liu, Z., Jifeng, H., Li, X. (2005). rCOS: Refinement of Component and Object Systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2004. Lecture Notes in Computer Science, vol 3657. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11561163_9
Download citation
DOI: https://doi.org/10.1007/11561163_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29131-2
Online ISBN: 978-3-540-31939-9
eBook Packages: Computer ScienceComputer Science (R0)