{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T18:28:46Z","timestamp":1772044126289,"version":"3.50.1"},"publisher-location":"Cham","reference-count":92,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319296272","type":"print"},{"value":"9783319296289","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29628-9_4","type":"book-chapter","created":{"date-parts":[[2016,2,28]],"date-time":"2016-02-28T21:04:31Z","timestamp":1456693471000},"page":"152-255","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Model-Driven Design of Object and Component Systems"],"prefix":"10.1007","author":[{"given":"Zhiming","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaohong","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,3,1]]},"reference":[{"key":"4_CR1","unstructured":"Hamilton, M.: The engineer who took the apollo to the moon. https:\/\/medium.com\/@verne\/margaret-hamilton-the-engineer-who-took-the-apollo-to-the-moon-7d550c73d3fa"},{"key":"4_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"4_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-642-35743-5_15","volume-title":"Formal Aspects of Component Software","author":"S Limet","year":"2012","unstructured":"Limet, S., Robert, S., Turki, A.: Controlling an iteration-wise coherence in dataflow. In: Arbab, F., \u00d6lveczky, P.C. (eds.) FACS 2011. LNCS, vol. 7253, pp. 241\u2013258. Springer, Heidelberg (2012)"},{"key":"4_CR5","volume-title":"Service-Oriented Modeling: Service Analysis, Design, and Architecture","author":"M Bell","year":"2008","unstructured":"Bell, M.: Service-Oriented Modeling: Service Analysis, Design, and Architecture. Wiley & Sons, New Jersey (2008)"},{"key":"4_CR6","volume-title":"Object-Oriented Analysis and Design with Applications","author":"G Booch","year":"1994","unstructured":"Booch, G.: Object-Oriented Analysis and Design with Applications. Addison-Wesley, Boston (1994)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Bowen, J.P., Hinchey, M.G.: Formal methods. In: Gonzalez, T.F., Diaz-Herrera, J., Tucker, A.B.(eds.) Computer Science Handbook, 3rd edn. Section XI, Software Engineering, vol. 1, Computer Science and Software Engineering, Part 8, Programming Languages, Chapter 71, pp. 1\u201325. CRC Press (2014)","DOI":"10.1201\/b16812-80"},{"issue":"4","key":"4_CR8","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1109\/MC.1987.1663532","volume":"20","author":"FP Brooks","year":"1987","unstructured":"Brooks, F.P.: No silver bullet: essence and accidents of software engineering. IEEE Comput. 20(4), 10\u201319 (1987)","journal-title":"IEEE Comput."},{"issue":"5","key":"4_CR9","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1109\/MS.1995.10042","volume":"12","author":"FP Brooks","year":"1995","unstructured":"Brooks, F.P.: The mythical man-month: after 20 years. IEEE Softw. 12(5), 57\u201360 (1995)","journal-title":"IEEE Softw."},{"key":"4_CR10","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: a Foundation. Addison-Wesley, Reading. (1988)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-540-75698-9_13","volume-title":"International Symposium on Fundamentals of Software Engineering","author":"X Chen","year":"2007","unstructured":"Chen, X., He, J., Liu, Z., Zhan, N.: A model of component-based programming. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 191\u2013206. Springer, Heidelberg (2007)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1007\/978-3-540-69507-3_71","volume-title":"SOFSEM 2007: Theory and Practice of Computer Science","author":"X Chen","year":"2007","unstructured":"Chen, X., Liu, Z., Mencl, V.: Separation of concerns and consistent integration in requirements modelling. In: van Leeuwen, J., Italiano, G.F., van der Hoek, W., Meinel, C., Sack, H., Pl\u00e1\u0161il, F. (eds.) SOFSEM 2007. LNCS, vol. 4362, pp. 819\u2013831. Springer, Heidelberg (2007)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-85289-6_6","volume-title":"The Common Component Modeling Example","author":"Z Chen","year":"2008","unstructured":"Chen, Z., et al.: Modelling with relational calculus of object and component systems - rCOS. In: Rausch, A., Reussner, R., Mirandola, R., Pl\u00e1\u0161il, F. (eds.) The Common Component Modeling Example. LNCS, vol. 5153, pp. 116\u2013145. Springer, Heidelberg (2008)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-75221-9_5","volume-title":"Formal Methods and Hybrid Real-Time Systems","author":"Z Chen","year":"2007","unstructured":"Chen, Z., Li, X., Liu, Z., Stolz, V., Yang, L.: Harnessing rCOS for tool support \u2014the CoCoME experience. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol. 4700, pp. 83\u2013114. Springer, Heidelberg (2007)"},{"issue":"4","key":"4_CR15","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1016\/j.scico.2008.08.003","volume":"74","author":"Z Chen","year":"2009","unstructured":"Chen, Z., Liu, Z., Ravn, A.P., Stolz, V., Zhan, N.: Refinement and verification in component-based model driven design. Sci. Comput. Program. 74(4), 168\u2013196 (2009)","journal-title":"Sci. Comput. Program."},{"key":"4_CR16","unstructured":"Chen, Z., Liu, Z., Stolz, V.: The rCOS tool. In: Fitzgerald, J., Larsen, P.G., Sahara, S. (eds.) Modelling and Analysis in VDM: Proceedings of the Fourth VDM\/Overture Workshop, pp. 15\u201324. No. CS-TR-1099 in Technical report Series, University of Newcastle upon Tyne (2008)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-11623-0_23","volume-title":"Fundamentals of Software Engineering","author":"Z Chen","year":"2010","unstructured":"Chen, Z., Morisset, C., Stolz, V.: Specification and validation of behavioural protocols in the rCOS modeler. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 387\u2013401. Springer, Heidelberg (2010)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"4_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"EW Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, New York (1990)"},{"issue":"10","key":"4_CR20","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1145\/355604.361591","volume":"15","author":"EW Dijkstra","year":"1972","unstructured":"Dijkstra, E.W.: The humble programmer. Commun. ACM 15(10), 859\u2013866 (1972). An ACM Turing Award lecture","journal-title":"Commun. ACM"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-642-39718-9_10","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2013","author":"R Dong","year":"2013","unstructured":"Dong, R., Zhan, N., Zhao, L.: An interface model of software components. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 159\u2013176. Springer, Heidelberg (2013)"},{"key":"4_CR22","unstructured":"Fischer, C.: Fault-tolerant programming by transformations. Ph.D. thesis, University of Warwick (1991)"},{"key":"4_CR23","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E Gamma","year":"1994","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Boston (1994)"},{"issue":"3","key":"4_CR24","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/11560647_5","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2005","author":"J He","year":"2005","unstructured":"He, J., Li, X., Liu, Z.: Component-based software engineering. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 70\u201395. Springer, Heidelberg (2005)"},{"key":"4_CR26","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/j.entcs.2006.05.022","volume":"160","author":"J He","year":"2006","unstructured":"He, J., Li, X., Liu, Z.: A theory of reactive components. Electr. Notes Theor. Comput. Sci. 160, 173\u2013195 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1\u20132","key":"4_CR27","first-page":"109","volume":"365","author":"J He","year":"2006","unstructured":"He, J., Liu, Z., Li, X.: rCOS: a refinement calculus of object systems. Theor. Comput. Sci. 365(1\u20132), 109\u2013142 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR28","volume-title":"Component-Based Software Engineering: Putting the Pieces Together","author":"GT Heineman","year":"2001","unstructured":"Heineman, G.T., Councill, W.T.: Component-Based Software Engineering: Putting the Pieces Together. Addison-Wesley Professional, Reading (2001)"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-85289-6_3","volume-title":"The Common Component Modeling Example","author":"S Herold","year":"2008","unstructured":"Herold, S., et al.: CoCoME - the common component modeling example. In: Rausch, A., Reussner, R., Mirandola, R., Pl\u00e1\u0161il, F. (eds.) The Common Component Modeling Example. LNCS, vol. 5153, pp. 16\u201353. Springer, Heidelberg (2008)"},{"issue":"10","key":"4_CR30","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"4_CR31","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)"},{"key":"4_CR32","volume-title":"Unifying Theories of Programming","author":"CAR Hoare","year":"1998","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Upper Saddle River (1998)"},{"key":"4_CR33","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"issue":"12","key":"4_CR34","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1109\/MC.2007.419","volume":"40","author":"GJ Holzmann","year":"2007","unstructured":"Holzmann, G.J.: Conquering complexity. IEEE Comput. 40(12), 111\u2013113 (2007)","journal-title":"IEEE Comput."},{"key":"4_CR35","volume-title":"My Life is Failure: 100 Things You Should Know to Be a Better Project Leader","author":"J Johnson","year":"2006","unstructured":"Johnson, J.: My Life is Failure: 100 Things You Should Know to Be a Better Project Leader. Standish Group International, West Yarmouth (2006)"},{"key":"4_CR36","volume-title":"Systematic Software Development using VDM","author":"CB Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development using VDM. Prentice Hall, Upper Saddle River (1990)"},{"issue":"1","key":"4_CR37","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/s11704-012-2901-5","volume":"6","author":"W Ke","year":"2012","unstructured":"Ke, W., Li, X., Liu, Z., Stolz, V.: rCOS: a formal model-driven engineering method for component-based software. Front. Comput. Sci. China 6(1), 17\u201339 (2012)","journal-title":"Front. Comput. Sci. China"},{"key":"4_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-10373-5_18","volume-title":"Formal Methods and Software Engineering","author":"W Ke","year":"2009","unstructured":"Ke, W., Liu, Z., Wang, S., Zhao, L.: A graph-based operational semantics of OO programs. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 347\u2013366. Springer, Heidelberg (2009)"},{"issue":"2","key":"4_CR39","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1109\/JSYST.2014.2322503","volume":"9","author":"S Khaitan","year":"2014","unstructured":"Khaitan, S.: Design techniques and applications of cyber physical systems: a survey. IEEE Syst. J. 9(2), 350\u2013365 (2014)","journal-title":"IEEE Syst. J."},{"key":"4_CR40","volume-title":"The Rational Unified Process Made Easy: a Practitioner\u2019s Guide to the RUP","author":"P Kroll","year":"2003","unstructured":"Kroll, P., Kruchten, P.: The Rational Unified Process Made Easy: a Practitioner\u2019s Guide to the RUP. Addison-Wesley, Boston (2003)"},{"key":"4_CR41","volume-title":"Specifying Systems: the TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: the TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"4_CR42","volume-title":"Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and the Unified Process","author":"C Larman","year":"2001","unstructured":"Larman, C.: Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and the Unified Process, 2nd edn. Prentice-Hall, Upper Saddle River (2001)","edition":"2"},{"key":"4_CR43","doi-asserted-by":"crossref","unstructured":"Lee, E.: Cyber physical systems: design challenges. Technical report No. UCB\/EECS-2008-8, University of California, Berkeley (2008)","DOI":"10.1109\/ISORC.2008.25"},{"issue":"7","key":"4_CR44","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/MC.1993.274940","volume":"26","author":"NG Leveson","year":"1993","unstructured":"Leveson, N.G., Turner, C.S.: An investigation of the Therac-25 accidents. IEEE Comput. 26(7), 18\u201341 (1993)","journal-title":"IEEE Comput."},{"key":"4_CR45","doi-asserted-by":"crossref","unstructured":"Li, D., Li, X., Liu, Z., Stolz, V.: Interactive transformations from object-oriented models to component-based models. Technical report 451, IIST, United Nations University, Macao (2011)","DOI":"10.1007\/978-3-642-35743-5_7"},{"key":"4_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-642-35743-5_7","volume-title":"Formal Aspects of Component Software","author":"D Li","year":"2012","unstructured":"Li, D., Li, X., Liu, Z., Stolz, V.: Interactive transformations from object-oriented models to component-based models. In: Arbab, F., \u00d6lveczky, P.C. (eds.) FACS 2011. LNCS, vol. 7253, pp. 97\u2013114. Springer, Heidelberg (2012)"},{"key":"4_CR47","doi-asserted-by":"crossref","unstructured":"Li, D., Li, X., Liu, Z., Stolz, V.: Support formal component-based development with UML profile. In: 22nd Australian Conference on Software Engineering (ASWEC 2013), Melbourne, pp. 191\u2013200. IEEE Computer Society, 4\u20137 June 2013","DOI":"10.1109\/ASWEC.2013.31"},{"issue":"11","key":"4_CR48","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1109\/MCOM.2011.6069711","volume":"49","author":"X Li","year":"2011","unstructured":"Li, X., Lu, R., Liang, X., Shen, X., Chen, J., Lin, X.: Smart community: an internet of things application. Commun. Mag. 49(11), 68\u201375 (2011)","journal-title":"Commun. Mag."},{"key":"4_CR49","doi-asserted-by":"crossref","unstructured":"Li, X., Liu, Z., He, J.: Formal and use-case driven requirement analysis in UML. In: 25th International Computer Software and Applications Conference (COMPSAC 2001), Invigorating Software Development, Chicago, pp. 215\u2013224. IEEE Computer Society, 8\u201312 October 2001","DOI":"10.1109\/CMPSAC.2001.960619"},{"key":"4_CR50","doi-asserted-by":"crossref","unstructured":"Li, X., Liu, Z., He, J.: A formal semantics of UML sequence diagram. In: 15th Australian Software Engineering Conference (ASWEC 2004), Melbourne, pp. 168\u2013177. IEEE Computer Society, 13\u201316 April 2004","DOI":"10.1109\/ASWEC.2004.1290469"},{"key":"4_CR51","unstructured":"Li, X., Liu, Z., He, J.: Consistency checking of UML requirements. In: 10th International Conference on Engineering of Complex Computer Systems, pp. 411\u2013420. IEEE Computer Society (2005)"},{"key":"4_CR52","doi-asserted-by":"crossref","unstructured":"Liu, J., Liu, Z., He, J., Li, X.: Linking UML models of design and requirement. In: Proceedings of the 2004 Australian Software Engineering Conference, pp. 329\u2013338. IEEE Computer Society (2004)","DOI":"10.1109\/ASWEC.2004.1290486"},{"key":"4_CR53","unstructured":"Liu, Z.: Software development with UML. Technical Report 259, IIST, United Nations University, P.O. Box 3058, Macao (2002)"},{"key":"4_CR54","unstructured":"Liu, Z., Chen, X.: Interface-driven design in evolving component-based architectures, workshop of the 25 Anniversary of ProCoS, Proceedings to be Published in Springer Lecture Notes in Computer Science (2015)"},{"key":"4_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-540-39893-6_36","volume-title":"Formal Methods and Software Engineering","author":"Z Liu","year":"2003","unstructured":"Liu, Z., He, J., Li, X., Chen, Y.F.: A relational model for formal object-oriented requirement analysis in UML. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 641\u2013664. Springer, Heidelberg (2003)"},{"issue":"5","key":"4_CR56","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/BF01211393","volume":"4","author":"Z Liu","year":"1992","unstructured":"Liu, Z., Joseph, M.: Transformation of programs for fault-tolerance. Form. Asp. Comput. 4(5), 442\u2013469 (1992)","journal-title":"Form. Asp. Comput."},{"issue":"1","key":"4_CR57","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/314602.314605","volume":"21","author":"Z Liu","year":"1999","unstructured":"Liu, Z., Joseph, M.: Specification and verification of fault-tolerance, timing, and scheduling. ACM Trans. Program. Lang. Syst. 21(1), 46\u201389 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-642-14521-6_14","volume-title":"Unifying Theories of Programming","author":"Z Liu","year":"2010","unstructured":"Liu, Z., Kang, E.Y., Zhan, N.: Composition and refinement of components. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 238\u2013257. Springer, Heidelberg (2010)"},{"key":"4_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1007\/3-540-36103-0_54","volume-title":"Formal Methods and Software Engineering","author":"Z Liu","year":"2002","unstructured":"Liu, Z., Li, X., He, J.: Using transition systems to unify UML models. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 535\u2013547. Springer, Heidelberg (2002)"},{"key":"4_CR60","doi-asserted-by":"crossref","unstructured":"Liu, Z., Mencl, V., Ravn, A.P., Yang, L.: Harnessing theories for tool support. In: Proceedings of the Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006), pp. 371\u2013382. IEEE Computer Society, full version as UNU-IIST Technical report 343 (2006)","DOI":"10.1109\/ISoLA.2006.49"},{"key":"4_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-642-11623-0_3","volume-title":"Fundamentals of Software Engineering","author":"Z Liu","year":"2010","unstructured":"Liu, Z., Morisset, C., Stolz, V.: rCOS: theory and tool for component-based model driven development. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 62\u201380. Springer, Heidelberg (2010)"},{"key":"4_CR62","unstructured":"Long, Q., Liu, Z., Li, X., He, J.: Consistent code generation from UML models. In: Australian Software Engineering Conference, pp. 23\u201330. IEEE Computer Society, UNU-IIST TR 319 (2005)"},{"key":"4_CR63","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-540-88479-8_23","volume-title":"International Symposium on Leveraging Applications of Formal Methods, Verification and Validation","author":"Q Long","year":"2008","unstructured":"Long, Q., Qiu, Z., Liu, Z.: Formal use of design patterns and refactoring. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. Communications in Computer and Information Science, vol. 17, pp. 323\u2013338. Springer, Berlin (2008)"},{"issue":"3","key":"4_CR64","first-page":"219","volume":"2","author":"NA Lynch","year":"1989","unstructured":"Lynch, N.A., Tuttle, M.R.: An introduction to input\/output automata. CWI Q. 2(3), 219\u2013246 (1989)","journal-title":"CWI Q."},{"key":"4_CR65","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)"},{"key":"4_CR66","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)"},{"key":"4_CR67","unstructured":"Naur, P., Randell, B. (eds.): Software engineering: report of a conference sponsored by the NATO science committee, Garmisch, 7\u201311 October 1968, Brussels, Scientific Affairs Division, NATO (1969)"},{"key":"4_CR68","volume-title":"Semantics with Applications. A Formal Introduction","author":"H Nielson","year":"1993","unstructured":"Nielson, H., Nielson, F.: Semantics with Applications. A Formal Introduction. Wiley, Chichester (1993)"},{"key":"4_CR69","doi-asserted-by":"crossref","unstructured":"Nuseibeh, B., Easterbrook, S.: Requirements engineering: a roadmap. In: Proceedings of the Conference on the Future of Software Engineering, ICSE 2000, pp. 35\u201346. ACM, New York (2000)","DOI":"10.1145\/336512.336523"},{"key":"4_CR70","unstructured":"Object Managment Group: Model driven architecture - a technical perspective, document number ORMSC, 01 July 2001"},{"issue":"10","key":"4_CR71","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1145\/363717.363722","volume":"10","author":"A Oettinger","year":"1967","unstructured":"Oettinger, A.: The hardware-software complementarity. Commun. ACM 10(10), 604\u2013606 (1967)","journal-title":"Commun. ACM"},{"key":"4_CR72","doi-asserted-by":"crossref","unstructured":"Palomar, E., Liu, Z., Bowen, J.P., Zhang, Y., Maharjan, S.: Component-based modelling for sustainable and scalable smart meter networks. In: Proceeding of IEEE International Symposium on a World of Wireless, Mobile and Multimedia Networks, WoWMoM 2014, Sydney, pp. 1\u20136, 19 June 2014","DOI":"10.1109\/WoWMoM.2014.6918927"},{"key":"4_CR73","volume-title":"The Peter Pyramid","author":"L Peter","year":"1986","unstructured":"Peter, L.: The Peter Pyramid. William Morrow, New York (1986)"},{"issue":"3","key":"4_CR74","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1145\/356698.356702","volume":"9","author":"JL Peterson","year":"1977","unstructured":"Peterson, J.L.: Petri Nets. ACM Comput. Surv. 9(3), 223\u2013252 (1977)","journal-title":"ACM Comput. Surv."},{"issue":"61","key":"4_CR75","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jlap.2004.03.009","volume":"60","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: The origins of structural operational semantics. J. Log. Algebr. Program. 60(61), 3\u201315 (2004)","journal-title":"J. Log. Algebr. Program."},{"key":"4_CR76","volume-title":"Software Engineering: A Practitioner\u2019s Approach","author":"RS Pressman","year":"2005","unstructured":"Pressman, R.S.: Software Engineering: A Practitioner\u2019s Approach. The McGraw-Hill Companies, New York (2005)"},{"key":"4_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Symposium on Programming","author":"JP Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Symposium on Programming. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"4_CR78","unstructured":"Randell, B., Buxton, J. (eds.): Software engineering: report of a conference sponsored by the NATO science committee, Rome, Italy, 27\u201331 October 1969, Brussels, Scientific Affairs Division, NATO (1969)"},{"key":"4_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-85289-6_1","volume-title":"The Common Component Modeling Example","author":"A Rausch","year":"2008","unstructured":"Rausch, A., Reussner, R., Mirandola, R., Pl\u00e1\u0161il, F.: Introduction. In: Rausch, A., Reussner, R., Mirandola, R., Pl\u00e1\u0161il, F. (eds.) The Common Component Modeling Example. LNCS, vol. 5153, pp. 1\u20133. Springer, Heidelberg (2008)"},{"key":"4_CR80","unstructured":"Rayl, A.: NASA engineers and scientists-transforming dreams into reality (2008)"},{"key":"4_CR81","unstructured":"Robinson, K.: Ariane 5: flight 501 failure - a case study (2011)"},{"key":"4_CR82","volume-title":"Theory and Practice of Concurrency","author":"AW Roscoe","year":"1997","unstructured":"Roscoe, A.W.: Theory and Practice of Concurrency. Prentice-Hall, Upper Saddle River (1997)"},{"key":"4_CR83","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1162\/rest.88.2.324","volume":"88","author":"M Shapiro","year":"2006","unstructured":"Shapiro, M.: Smart cities: quality of life, productivity, and the growth effects of human capital. Rev. Econ. Stat. 88, 324\u2013335 (2006)","journal-title":"Rev. Econ. Stat."},{"key":"4_CR84","volume-title":"Software Engineering","author":"I Sommerville","year":"2001","unstructured":"Sommerville, I.: Software Engineering, 6th edn. Pearson Education Ltd., England (2001)","edition":"6"},{"key":"4_CR85","volume-title":"The Z Notation: a Reference Manual","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: a Reference Manual, 2nd edn. Prentice Hall, Upper Saddle River (1992)","edition":"2"},{"key":"4_CR86","unstructured":"Stellman, A., Greene, J.: Applied Software Project Management. O\u2019Reilly Media (2005)"},{"key":"4_CR87","volume-title":"Denotational Semantics: the Scott-Strachey Approach to Programming Language Semantics","author":"JE Stoy","year":"1977","unstructured":"Stoy, J.E.: Denotational Semantics: the Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge (1977)"},{"key":"4_CR88","volume-title":"Component Software: Beyond Object-Oriented Programming","author":"C Szyperski","year":"2002","unstructured":"Szyperski, C.: Component Software: Beyond Object-Oriented Programming, 2nd edn. Addison-Wesley Longman Publishing Co. Inc., Boston (2002)","edition":"2"},{"key":"4_CR89","volume-title":"Software-Intensive Systems and New Computing Paradigms - Challenges and Visions","year":"2008","unstructured":"Wirsing, M., Ban\u00e2tre, J.P., H\u00f6lzl, M.M., Rauschmayer, A. (eds.): Software-Intensive Systems and New Computing Paradigms - Challenges and Visions, vol. 5380. Springer, New York (2008)"},{"key":"4_CR90","doi-asserted-by":"crossref","unstructured":"Yang, L., Stolz, V.: Integrating refinement into software development tools. In: Pu, G., Stolz, V. (eds.) 1st International Workshop on Harnessing Theories for Tool Support in Software. Electronic Notes in Theoretical Computer Science, vol. 207, pp. 69\u201388. Elsevier, Amsterdam, UNU-IIST TR 385 (2008)","DOI":"10.1016\/j.entcs.2008.03.086"},{"issue":"1\u20132","key":"4_CR91","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/s00165-007-0067-y","volume":"21","author":"L Zhao","year":"2009","unstructured":"Zhao, L., Liu, X., Liu, Z., Qiu, Z.: Graph transformations for object-oriented refinement. Form. Asp. Comput. 21(1\u20132), 103\u2013131 (2009)","journal-title":"Form. Asp. Comput."},{"key":"4_CR92","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/978-3-642-39698-4_23","volume-title":"Theories of Programming and Formal Methods","author":"L Zhao","year":"2013","unstructured":"Zhao, L., Wang, S., Liu, Z.: Graph-based object-oriented hoare logic. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 374\u2013393. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29628-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T12:03:22Z","timestamp":1770379402000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-29628-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296272","9783319296289"],"references-count":92,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29628-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"1 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}