rCOS: a formal model-driven engineering method for component-based software

doi:10.1007/s11704-012-2901-5

Front Comput Sci

0, Vol.

Issue () : 17-39 https://doi.org/10.1007/s11704-012-2901-5

RESEARCH ARTICLE

rCOS: a formal model-driven engineering method for component-based software

Wei KE^1,5, Xiaoshan LI², Zhiming LIU³(

), Volker STOLZ^3,4

1. School of Computer Science and Engineering, Beihang University, Beijing 100191, China; 2. Faculty of Science and Technology, University of Macau, Macau, China; 3. UNU-IIST, Macau, China; 4. Department of Informatics, University of Oslo, Oslo 0316, Norway; 5. Macao Polytechnic Institute, Macau, China

Download: PDF(772 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

Model-driven architecture (MDA) has become a main stream technology for software-intensive system design. The main engineering principle behind it is that the inherent complexity of software development can only be mastered by building, analyzing and manipulating system models. MDA also deals with system complexity by providing component-based design techniques, allowing independent component design, implementation and deployment, and then system integration and reconfiguration based on component interfaces. The model of a system in any stage is an integration of models of different viewpoints. Therefore, for a model-driven method to be applied effectively, it must provide a body of techniques and an integrated suite of tools for model construction, validation, and transformation. This requires a number of modeling notations for the specification of different concerns and viewpoints of the system. These notations should have formally defined syntaxes and a unified theory of semantics. The underlying theory of the method is needed to underpin the development of tools and correct use of tools in software development, as well as to formally verify and reason about properties of systems in mission-critical applications. The modeling notations, techniques, and tools must be designed so that they can be used seamlessly in supporting development activities and documentation of artifacts in software design processes. This article presents such a method, called the rCOS, focusing on the models of a system at different stages in a software development process, their semantic integration, and how they are constructed, analyzed, transformed, validated, and verified.

Keywords component-based design models model transformations verification tool support

Corresponding Author(s): LIU Zhiming,Email:z.liu@iist.unu.edu

Issue Date: 01 February 2012

Cite this article:

Wei KE,Xiaoshan LI,Zhiming LIU, et al. rCOS: a formal model-driven engineering method for component-based software[J]. Front Comput Sci, 0, (): 17-39.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-012-2901-5
https://academic.hep.com.cn/fcs/EN/Y0/V/I/17

1	Dijkstra EW. The humble programmer. Communications of the ACM , 1972, 15(10): 859-866 , ACM Turing Award lecture doi: 10.1145/355604.361591
2	Brooks Jr F P. No silver bullet: Essence and accidents of software engineering. IEEE Computer , 1987, 20(4): 10-19 doi: 10.1109/MC.1987.1663532
3	Booch G. Object-Oriented Analysis and Design with Applications. Boston: Addison-Wesley, 1994
4	Brooks Jr F P. The mythical man-month: After 20 years. IEEE Software , 1995, 12(5): 57-60
5	Holzmann G J. Conquering complexity. IEEE Computer , 2007, 40(12): 111-113 doi: 10.1109/MC.2007.419
6	Wirsing M, Banatre J P, H?lzl M, Rauschmayer A. Software-Intensive Systems and New Computing Paradigms — Challenges and Visions. Lecture Notes in Computer Science , 2008, 5380
7	Peter L. The Peter Pyramid. New York: William Morrow, 1986
8	Leveson N G, Turner C S. An investigation of the Therac-25 accidents. IEEE Computer , 1993, 26(7): 18-41 doi: 10.1109/MC.1993.274940
9	Robinson K. Ariane 5: Flight 501 failure — A case study. http://www.cse.unsw.edu.au/～se4921/PDF/ariane5-article.pdf, 2011
10	Johnson J. My Life Is Failure: 100 Things You Should Know to Be a Better Project Leader. West Yarmouth: Standish Group International, 2006
11	Szyperski C. Component Software: Beyond Object-Oriented Program ming. Boston: Addison-Wesley, 1997
12	Object Management Group. Model driven architecture — A technical perspective. Document number ORMSC 2001-07-01 , 2001
13	Liu Z, Kang E, Zhan N. Composition and refinement of components. In: Butterfield A, eds. Post Event Proceedings of UTP08. Lecture Notes in Computer Science , 2009, 5713
14	Chen Z, Liu Z, Ravn A P, Stolz V, Zhan N. Refinement and verification in component-based model driven design. Science of Computer Programming , 2009, 74(4): 168-196 doi: 10.1016/j.scico.2008.08.003
15	Zhao L, Liu X, Liu Z, Qiu Z. Graph transformations for object-oriented refinement. Formal Aspects of Computing , 2009, 21(1-2): 103-131 doi: 10.1007/s00165-007-0067-y
16	Chen X, He J, Liu Z, Zhan N. A model of component-based programming. In: Arbab F, Sirjani M, eds. International Symposium on Fundamentals of Software Engineering, Lecture Notes in Computer Science , 2007, 4767: 191-206 doi: 10.1007/978-3-540-75698-9_13
17	Hoare C A R. An axiomatic basis for computer programming. Communications of the ACM , 1969, 12(10): 576-580 doi: 10.1145/363235.363259
18	Chen X, Liu Z, Mencl V. Separation of concerns and consistent integration in requirements modelling. In: Leeuwen J, Italiano G F, Hoek W, Meinel C, Sack H, Plá?il F, eds. Proceedings of 33rd Conference on Current Trends in Theory and Practice of Computer Science. Lecture Notes in Computer Science , 2007, 4362
19	Liu J, Liu Z, He J, Li X. Linking UML models of design and requirement. In: Proceedings of the 2004 Australian Software Engineering Conference . Washington: IEEE Computer Society, 2004, 329-338
20	Li X, Liu Z, He J. Consistency checking of UML requirements. In: Proceedings of 10th International Conference on Engineering of Complex Computer Systems . Washington: IEEE Computer Society, 2005, 411-420
21	He J, Li X, Liu Z. A theory of reactive components. Electronic Notes in Theoretical Computer Science , 2006, 160: 173-195 doi: 10.1016/j.entcs.2006.05.022
22	He J, Liu Z, LiX. rCOS:Arefinement calculus of object systems. Theoretical Computer Science , 2006, 365(1-2): 109-142 doi: 10.1016/j.tcs.2006.07.034
23	Ke W, Liu Z, Wang S, Zhao L. A graph-based operational semantics of OO programs. In: Proceedings of 11th International Conference on Formal Engineering Methods. Lecture Notes in Computer Science , 2009, 5885: 347-366 doi: 10.1007/978-3-642-10373-5_18
24	Spivey J M. The Z Notation: A Reference Manual. 2nd ed. Upper Saddle River: Prentice Hall, 1992
25	Jones C B. Systematic Software Development Using VDM. Upper Saddle River: Prentice Hall, 1990
26	Leavens G T. JML’s rich, inherited specifications for behavioral subtypes. In: Liu Z, He J, eds. Proceedings of 8th International Conference on Formal Engineering Methods. Lecture Notes in Computer Science , 2006, 4260: 2-34
27	Hoare C A R. Communicating Sequential Processes. Upper Saddle River: Prentice-Hall, 1985
28	Roscoe AW. Theory and Practice of Concurrency. Upper Saddle River: Prentice-Hall, 1997
29	Alfaro Ld, Henzinger T A. Interface automata. SIGSOFT Software Engineering Notes , 2001, 26(5): 109-120 doi: 10.1145/503271.503226
30	Liu Z, Joseph M. Specification and verification of fault tolerance, timing, and scheduling. ACM Transactions on Programming Languages and Systems , 1999, 21(1): 46-89 doi: 10.1145/314602.314605
31	Hoare C A R, He J. Unifying Theories of Programming. Upper Saddle River: Prentice-Hall, 1998
32	Dijkstra E W, Scholten C S. Predicate Calculus and Program Semantics. New York: Springer-Verlag, 1990
33	Fowler M. Refactoring — Improving the Design of Existing Code. Menlo Park: Addison-Wesley, 1999
34	Larman C. Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and the Unified Process. 3rd ed . Upper Saddle River: Prentice-Hall, 2005
35	Chandy K M, Misra J. Parallel Program Design: A Foundation. Reading: Addison-Wesley, 1988
36	Back R J R, von Wright J. Trace refinement of action systems. In: Proceedings of 5th International Conference on Concurrency Theory. Lecture Notes in Computer Science , 1994, 836: 367-384 doi: 10.1007/BFb0015020
37	Lamport L. The temporal logic of actions. ACM Transactions on Programming Languages and Systems , 1994, 16(3): 872-923 doi: 10.1145/177492.177726
38	Milner R. Communication and Concurrency. Upper Saddle River: Prentice-Hall, 1989
39	Lynch N A, Tuttle M R. An introduction to input/output automata. CWI Quarterly , 1989, 2(3): 219-246
40	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/OvertureWorkshop, number CSTR-1099 in Technical Report Series . Newcastle: University of Newcastle Upon Tyne, 2008, 15-24
41	Li D, Li X, Liu Z, Stolz V. Interactive transformations from objectoriented models to component-based models. Technical Report 451, IIST, United Nations University, Macao , 2011
42	Chen Z, Hannousse A H, Hung D V, Knoll I, Li X, Liu Y, Liu Z, Nan Q, Okika J C, Ravn A P, Stolz V, Yang L, Zhan N. Modelling with relational calculus of object and component systems-rCOS. In: Rausch A, Reussner R, Mirandola R, Plasil F, eds. The Common Component Modeling Example. Lecture Notes in Computer Science , 2008, 5153 (Chapter 3): 116-145
43	Li X, Liu Z, Sch?f M, Yin L. AutoPA: Automatic prototyping from requirements. In: Margaria T, Steffen B, eds. Proceedings of 4th International Conference on Leveraging Applications of Formal Methods. Lecture Notes in Computer Science , 2010, 6415: 609-624
44	Object Management Group. Object constraint language, version 2.0, May2006
45	Warmer J, Kleppe A. The Object Constraint Language: Precise Modeling with UML. Boston: Addison-Wesley, 1999
46	Chen Z, Morisset C, Stolz V. Specification and validation of behavioural protocols in the rCOS modeler. In: Arbab F, Sirjani M, eds. Proceedings of 3rd IPM International Conference on Fundamentals of Software Engineering. Lecture Notes in Computer Science , 2009, 5961: 387-401
47	Liu Z, Morisset C, Wang S. A graph-based implementation for mechanized refinement calculus of oo programs. In: Davies J, Silva L, Silva Sim?o Ad, eds. Proceedings of 13th Brazilian Symposium on Formal Methods. Lecture Notes in Computer Science , 2010, 6527: 258-273
48	Lei B, Li X, Liu Z, Morisset C, Stolz V. Robustness testing for software components. Science of Computer Programming , 2010, 75(10): 879-897 doi: 10.1016/j.scico.2010.02.005
49	Xiong X, Liu J, Ding Z. Design and verification of a trustable medical system. In: Johnsen E B, Stolz V, eds. Proceedings of 3rd International Workshop on Harnessing Theories for Tool Support in Software. Elec tronic Notes in Theoretical Computer Science , 2010, 266: 77-92
50	Liu J, He J. Reactive component based service-oriented design-a case study. In: Proceedings of 11th IEEE International Conference on Engineering of Complex Computer Systems . Washington: IEEE Computer Society, 2006, 27-36
51	Bertolini C, Liu Z, Sch?f M, Stolz V. Towards a formal integrated model of collaborative healthcare workflows. Technical Report 450, IIST, United Nations University, Macao, 2011. In: Proceedings of 1st International Symposium on Foundations of Health Information Engineering and Systems (In press)

[1]	Zhao-Hui LI, Xin-Yu FENG. A program logic for obstruction-freedom[J]. Front. Comput. Sci., 2024, 18(6): 186208-.
[2]	Shiwei LU, Ruihu LI, Wenbin LIU. FedDAA: a robust federated learning framework to protect privacy and defend against adversarial attack[J]. Front. Comput. Sci., 2024, 18(2): 182307-.
[3]	Abdelfettah MAATOUG, Ghalem BELALEM, Saïd MAHMOUDI. A location-based fog computing optimization of energy management in smart buildings: DEVS modeling and design of connected objects[J]. Front. Comput. Sci., 2023, 17(2): 172501-.
[4]	Shahbaz ALI, Hailong SUN, Yongwang ZHAO. Model learning: a survey of foundations, tools and applications[J]. Front. Comput. Sci., 2021, 15(5): 155210-.
[5]	Wangli HAO, Ian Max ANDOLINA, Wei WANG, Zhaoxiang ZHANG. Biologically inspired visual computing: the state of the art[J]. Front. Comput. Sci., 2021, 15(1): 151304-.
[6]	Zhumin CHEN, Xueqi CHENG, Shoubin DONG, Zhicheng DOU, Jiafeng GUO, Xuanjing HUANG, Yanyan LAN, Chenliang LI, Ru LI, Tie-Yan LIU, Yiqun LIU, Jun MA, Bing QIN, Mingwen WANG, Jirong WEN, Jun XU, Min ZHANG, Peng ZHANG, Qi ZHANG. Information retrieval: a view from the Chinese IR community[J]. Front. Comput. Sci., 2021, 15(1): 151601-.
[7]	Daian YUE, Vania JOLOBOFF, Frédéric MALLET. TRAP: trace runtime analysis of properties[J]. Front. Comput. Sci., 2020, 14(3): 143201-.
[8]	Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[9]	Tun LI, Jun YE, Qingping TAN. Towards functional verifying a family of SystemC TLMs[J]. Front. Comput. Sci., 2020, 14(1): 53-66.
[10]	Yan LI, Shiguang SHAN, Ruiping WANG, Zhen CUI, Xilin CHEN. Fusing magnitude and phase features with multiple face models for robust face recognition[J]. Front. Comput. Sci., 2018, 12(6): 1173-1191.
[11]	Abdelkrim CHEBIEB, Yamine AIT AMEUR. A formal model for plastic human computer interfaces[J]. Front. Comput. Sci., 2018, 12(2): 351-375.
[12]	Houkui ZHOU, Huimin YU, Roland HU. Topic evolution based on the probabilistic topic model: a review[J]. Front. Comput. Sci., 2017, 11(5): 786-802.
[13]	Yongwang ZHAO, Zhibin YANG, Dianfu MA. A survey on formal specification and verification of separation kernels[J]. Front. Comput. Sci., 2017, 11(4): 585-607.
[14]	Zhiyi MA. An approach to improve the quality of object-oriented models from novice modelers through project practice[J]. Front. Comput. Sci., 2017, 11(3): 485-498.
[15]	Qiang LU,Zhicheng CUI,Yixin CHEN,Xiaoping CHEN. Extracting optimal actionable plans from additive tree models[J]. Front. Comput. Sci., 2017, 11(1): 160-173.

Viewed

Full text

Abstract

Cited

Shared

Discussed