nach oben

Erschienen in:

2024 | OriginalPaper | Buchkapitel

Formal Aspects of Component Software

An Overview on Concepts and Relations of Different Theories

verfasst von : Zhiming Liu, Jiadong Teng, Bo Liu

Erschienen in: Formal Aspects of Component Software

Verlag: Springer Nature Switzerland

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The International Symposium on Formal Aspects of Component Software (FACS) was inaugurated two decades ago in response to the major software development paradigm shift from structured development and object-oriented development to component-based software development (CBSD) and service-oriented architecture (SOA). FACS is dedicated to fostering a deeper understanding of the distinctive aspects, promoting research, education, technological advancement, and the practical application of CBSD technology. On the 20th anniversary of FACS, it is appropriate to briefly recall its background and history, thereby highlighting its contributions to the community. Taking this opportunity, we focus on the discussion to elucidate the important aspects of component software that require to be and have been considered in formal theories. Leveraging the refinement of component and object-oriented systems (rCOS) as a framework, we provide an overview of these formal theories and discuss their relationships. We intend to express a vision that different theories and methods are required for different aspects in a CBSD process, and also different formal theories are required even for a particular aspect. However, ensuring their consistent application remains a major challenge and this is a main barrier to the effective industry adoption of CBSD. Furthermore, we delineate emerging challenges and prospects associated with integrating formal methods for modelling and design human-cyber-physical systems (HCPS) - hybrid integration encompassing cyber systems, physical systems, and the mixed human and machine intelligence.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Challenges Engaging Formal CBSE in Industrial Applications

Nächstes Kapitel Overview on Constrained Multiparty Synchronisation in Team Automata

The first author of this paper is the founder of FACS.

At a time when there is lack of hardware support to remember the return address of the routine.

However, it should be noted that we are not aware of such an existing repository.

Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)

de Alfaro, L., Henzinger, T.A.: Interface automata. SIGSOFT Softw. Eng. Notes 26(5), 109–120 (2001)CrossRef

Arbab, F.: Coordinated composition of software components. In: Liu, Z., He, J. (eds.) Mathematical Frameworks for Component Software, pp. 35–68. World Scientific (2006)

Arbab, F., Jongmans, S.-S. (eds.): FACS 2019. LNCS, vol. 12018. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-40914-2CrossRef

Arbab, F., Ölveczky, P.C. (eds.): FACS 2011. LNCS, vol. 7253. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35743-5CrossRef

Bae, K., Ölveczky, P.C. (eds.): FACS 2018. LNCS, vol. 11222. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02146-7CrossRef

Baeten, J.C.M., Bravetti, M.: A generic process algebra. In: Algebraic Process Calculi: The First Twenty Five Years and Beyond. BRICS Notes Series NS-05-3 (2005)

Barbosa, L.S., Lumpe, M. (eds.): FACS 2010. LNCS, vol. 6921. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27269-1CrossRef

Braga, C., Ölveczky, P.C. (eds.): FACS 2015. LNCS, vol. 9539. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-28934-2CrossRef

10.

Broy, M.: A theory for requirements specifications and architecture design. In: Liu, Z., He, J. (eds.) Mathematical Frameworks for Component Software, pp. 119–154. World Scientific (2006)

11.

Broy, M., Wirsing, M.: On the algebraic extensions of abstract data types. In: Díaz, J., Ramos, I. (eds.) ICFPC 1981. LNCS, vol. 107, pp. 244–251. Springer, Heidelberg (1981). https://doi.org/10.1007/3-540-10699-5_101CrossRef

12.

Canal, C., Pasareanu, C.S. (eds.): Proceedings of the 5th International Workshop on Formal Aspects of Component Software, FACS 2008, Malaga, Spain, 10–12 September 2008, Electronic Notes in Theoretical Computer Science, vol. 260. Elsevier (2010). https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/260/suppl/C

13.

Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)

14.

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ášil, F. (eds.) SOFSEM 2007. LNCS, vol. 4362, pp. 819–831. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69507-3_71CrossRef

15.

Chen, Z., et al.: Modelling with relational calculus of object and component systems - rCOS. In: Rausch, A., Reussner, R., Mirandola, R., Plášil, F. (eds.) The Common Component Modeling Example. LNCS, vol. 5153, pp. 116–145. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85289-6_6CrossRef

16.

Chen, Z., Li, X., Liu, Z., Stolz, V., Yang, L.: Harnessing rCOS for tool support—the CoCoME experience. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol. 4700, pp. 83–114. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75221-9_5CrossRef

17.

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–196 (2009)MathSciNetCrossRef

18.

Dahl, O., Dijkstra, E., Hoare, C.: Structured Programming. Academic Press, Cambridge (1972)

19.

Fiadeiro, J.L., Liu, Z., Xue, J. (eds.): FACS 2013. LNCS, vol. 8348. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07602-7CrossRef

20.

Goldberg, A., Robson, D.: Smalltalk-80: The Language and Its Implementation. Addison-Wesley Longman Publishing Co. Inc., Boston (1983)

21.

He, J.: From CSP to hybrid systems. In: The Proceedings of A Classical Mind: Essays in Honour of C. A. R. Hoare. Prentice-Hall (1994)

22.

He, J., Li, X., Liu, Z.: A theory of reactive components. Electr. Notes Theor. Comput. Sci. 160, 173–195 (2006)CrossRef

23.

He, J., Liu, Z., Li, X.: rCOS: a refinement calculus of object systems. Theoret. Comput. Sci. 365(1–2), 109–142 (2006)MathSciNet

24.

Henzinger, T.A., Manna, Z., Pnueli, A.: Temporal proof methodologies for timed transition systems. Inf. Comput. 112(2), 273–337 (1994)MathSciNetCrossRef

25.

Herold, S., et al.: CoCoME - the common component modeling example. In: Rausch, A., Reussner, R., Mirandola, R., Plášil, F. (eds.) The Common Component Modeling Example. LNCS, vol. 5153, pp. 16–53. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85289-6_3CrossRef

26.

Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRef

27.

Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)CrossRef

28.

Holmegaard, J.P., Knudsen, J., Makowski, P., Ravn, A.P.: Formalisization in component-based developmen. In: Liu, Z., He, J. (eds.) Mathematical Frameworks for Component Software, pp. 271–295. World Scientific (2006)

29.

Ke, W., Liu, Z., Wang, S., Zhao, L.: A graph-based generic type system for object-oriented programs. Front. Comput. Sci. 7(1), 109–134 (2013)MathSciNetCrossRef

30.

Kouchnarenko, O., Khosravi, R. (eds.): FACS 2016. LNCS, vol. 10231. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57666-4CrossRef

31.

Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)CrossRef

32.

Lanese, I., Madelaine, E. (eds.): FACS 2014. LNCS, vol. 8997. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15317-9CrossRef

33.

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)

34.

Li, D., Li, X., Liu, Z., Stolz, V.: Interactive transformations from object-oriented models to component-based models. In: Arbab, F., Ölveczky, P.C. (eds.) FACS 2011. LNCS, vol. 7253, pp. 97–114. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35743-5_7CrossRef

35.

Li, X., Liu, Z., He, J.: A formal semantics of UML sequence diagram. In: 15th Australian Software Engineering Conference (ASWEC 2004), 13–16 April 2004, Melbourne, Australia, pp. 168–177. IEEE Computer Society (2004)

36.

Liu, Z.: Software development with UML. Technical report 259, IIST, United Nations University, P.O. Box 3058, Macao (2002)

37.

Liu, Z.: Linking formal methods in software development - a reflection on the development of rCOS. In: Bowen, J., Li, Q., Xu, Q. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 14080, pp. 52–84. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-40436-8_3CrossRef

38.

Liu, Z., Barbosa, L.S. (eds.): Proceedings of the International Workshop on Formal Aspects of Component Software, FACS 2005, Macao, 24–25 October 2005. Electronic Notes in Theoretical Computer Science, vol. 160. Elsevier (2006). https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/160/suppl/C

39.

Liu, Z., Bowen, J.P., Liu, B., Tyszberowicz, S., Zhang, T.: Software abstractions and human-cyber-physical systems architecture modelling. In: Bowen, J.P., Liu, Z., Zhang, Z. (eds.) SETSS 2019. LNCS, vol. 12154, pp. 159–219. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-55089-9_5CrossRef

40.

Chen, X., Liu, Z.: Towards interface-driven design of evolving component-based architectures. In: Hinchey, M.G., Bowen, J.P., Olderog, E.-R. (eds.) Provably Correct Systems. NMSSE, pp. 121–148. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-48628-4_6CrossRef

41.

Liu, Z., Jifeng, H., Li, X.: Contract oriented development of component software. In: Levy, J.-J., Mayr, E.W., Mitchell, J.C. (eds.) TCS 2004. IIFIP, vol. 155, pp. 349–366. Springer, Boston, MA (2004). https://doi.org/10.1007/1-4020-8141-3_28CrossRef

42.

Liu, Z., He, J., Li, X.: rCOS: a relational calculus for components. In: Liu, Z., He, J. (eds.) Mathematical Frameworks for Component Software, pp. 207–238. World Scientific (2006)

43.

Liu, Z., Jifeng, H., Li, X., Chen, Y.: 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–664. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-39893-6_36CrossRef

44.

Liu, Z., Jifeng, H. (eds.): Mathematical Frameworks for Component Software. World Scientific (2006)

45.

Liu, Z., Joseph, M.: Specification and verification of fault-tolerance, timing, and scheduling. ACM Trans. Program. Lang. Syst. 21(1), 46–89 (1999)CrossRef

46.

Liu, Z., Kang, E., Zhan, N.: Composition and refinement of components. In: Butterfield, A. (ed.) Post Event Proceedings of UTP08. LNCS, vol. 5713. Springer, Berlin (2009)

47.

Liu, Z., Morisset, C., Stolz, V.: A component-based access control monitor. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 339–353. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88479-8_24CrossRef

48.

Liu, Z., Stolz, V.: The rCOS method in a nutshell. In: Fitzgerald, J., Larsen, P.G., Sahara, S. (eds.) Modelling and Analysis in VDM: Proceedings of the Fourth VDM/Overture Workshop. No. CS-TR-1099 in Technical Report Series, Newcastle University (2008)

49.

Liu, Z., Wang, J.: Human-cyber-physical systems: concepts, challenges, and research opportunities. Frontiers Inf. Technol. Electron. Eng. 21(11), 1535–1553 (2020)CrossRef

50.

Liu, Z., Zhang, Z. (eds.): SETSS 2014. LNCS, vol. 9506. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-29628-9CrossRef

51.

Long, Q., Liu, Z., Li, X., He, J.: Consistent code generation from UML models. In: Australian Software Engineering Conference, pp. 23–30. IEEE Computer Society (2005)

52.

Lumpe, M., Madelaine, E. (eds.): Proceedings of the 4th International Workshop on Formal Aspects of Component Software, FACS 2007, Sophia-Antipolis, France, 19–21 September 2007. Electronic Notes in Theoretical Computer Science, vol. 215. Elsevier (2008). https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/215/suppl/C

53.

Lynch, N., Segala, R., Vaandrager, F.: Hybrid I/O automata. Inf. Comput. 185, 105–157 (2003)MathSciNetCrossRef

54.

Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Q. 2(3), 219–246 (1989)MathSciNet

55.

McIlroy, M.D.: Mass produced software components. In: Software Engineering: Report of a Conference Sponsored by the NATO Science Committee, Garmisch, Germany, 7–11 October 1968. Scientific Affairs Division, NATO (1969)

56.

Mencl, V., de Boer, F.S. (eds.): Proceedings of the Third International Workshop on Formal Aspects of Component Software, FACS 2006, Prague, Czech Republic, 20–22 September 2006. Electronic Notes in Theoretical Computer Science, vol. 182. Elsevier (2007). https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/182/suppl/C

57.

Meng, S., Schätz, B. (eds.): Proceedings of the 6th International Workshop on Formal Aspects of Component Software, FACS@FMWeek 2009, Eindhoven, The Netherlands, 2–3 November 2009. Electronic Notes in Theoretical Computer Science, vol. 263. Elsevier (2010). https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/263/suppl/C

58.

Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Hoboken (1997)

59.

Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)

60.

Misra, J.: Orchestration. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 5–12. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07602-7_2CrossRef

61.

Palomar, E., Chen, X., Liu, Z., Maharjan, S., Bowen, J.P.: Component-based modelling for scalable smart city systems interoperability: a case study on integrating energy demand response systems. Sensors 16(11), 1810 (2016)CrossRef

62.

Păsăreanu, C.S., Salaün, G. (eds.): FACS 2012. LNCS, vol. 7684. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35861-6CrossRef

63.

Proença, J., Lumpe, M. (eds.): FACS 2017. LNCS, vol. 10487. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68034-7CrossRef

64.

Roscoe, A.W.: Theory and Practice of Concurrency. Prentice-Hall, Upper Saddle River (1997)

65.

Salaün, G., Wijs, A. (eds.): FACS 2021. LNCS, vol. 13077. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-90636-8CrossRef

66.

Szyperski, C.: Component Software: Beyond Object-Oriented Programming, 2nd edn. Addison-Wesley Longman Publishing Co. Inc., Boston (2002)

67.

Tang, X., Zhang, M., Liu, W., Du, B., Liu, Z.: Towards a model of human-cyber-physical automata and a synthesis framework for control policies. J. Syst. Archit. 144, 102989 (2023)CrossRef

68.

Tarifa, S.L.T., Proença, J. (eds.): FACS 2022. LNCS, vol. 13712. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-20872-0CrossRef

69.

Wheeler, D.J.: The use of sub-routines in programmes. In: Proceedings of the 1952 ACM National Meeting, Pittsburgh, USA, p. 235. ACM (1952)

70.

Yang, Y., Li, X., Ke, W., Liu, Z.: Automated prototype generation from formal requirements model. IEEE Trans. Reliab. 69(2), 632–656 (2020)CrossRef

71.

Zhang, M., Liu, W., Tang, X., Du, B., Liu, Z.: Human-cyber-physical automata and their synthesis. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) ICTAC 2022. LNCS, vol. 13572, pp. 36–41. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-17715-6_4CrossRef

72.

Zhao, L., Liu, X., Liu, Z., Qiu, Z.: Graph transformations for object-oriented refinement. Formal Aspects Comput. 21(1–2), 103–131 (2009)CrossRef

73.

Zou, L., Zhan, N., Wang, S., Fränzle, M., Qin, S.: Verifying simulink diagrams via a hybrid hoare logic prover. In: Ernst, R., Sokolsky, O. (eds.) Proceedings of the International Conference on Embedded Software, EMSOFT 2013, Montreal, QC, Canada, 29 September–4 October 2013, pp. 9:1–9:10. IEEE (2013). https://doi.org/10.1109/EMSOFT.2013.6658587

Titel: Formal Aspects of Component Software
verfasst von: Zhiming Liu
Jiadong Teng
Bo Liu
Verlag: Springer Nature Switzerland
Buch: Formal Aspects of Component Software
Print ISBN: 978-3-031-52182-9

Electronic ISBN: 978-3-031-52183-6

Copyright-Jahr: 2024
DOI: https://doi.org/10.1007/978-3-031-52183-6_9

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner