Top

Published in:

2024 | OriginalPaper | Chapter

Challenges Engaging Formal CBSE in Industrial Applications

Authors : Yi Li, Meng Sun

Published in: Formal Aspects of Component Software

Publisher: Springer Nature Switzerland

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Component-based software engineering (CBSE) is a widely used software development paradigm. With software systems becoming increasingly sophisticated, CBSE provides an effective approach to construct reusable, extensible, and maintainable software systems. Formal verification provides a rigorous and systematic approach to validate the correctness of software systems by mathematically proving properties or checking them exhaustively against specified requirements. Using formal verification techniques in component-based development can further enhance the correctness of the development process. However, the adoption of component-based development supported by formal methods is hardly widespread in the industry. It serves to a limited extent in domains with stringent requirements for safety and reliability. In this paper, we aim to analyze the successful application scenarios of formal methods in component-based development, identify the challenges faced during their application, and explore methods to further broaden their adoption.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter Formal Model Engineering of Distributed CPSs Using AADL: From Behavioral AADL Models to Multirate Hybrid Synchronous AADL

next chapter Formal Aspects of Component Software

Abrial, J., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)CrossRef

Ahmad, E., Dong, Y., Wang, S., Zhan, N., Zou, L.: Adding formal meanings to AADL with hybrid annex. In: Lanese, I., Madelaine, E. (eds.) FACS 2014. LNCS, vol. 8997, pp. 228–247. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15317-9_15CrossRef

Arbab, F.: Coordination for component composition. In: 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, pp. 15–40. Elsevier (2005)

Barke, S., James, M.B., Polikarpova, N.: Grounded copilot: how programmers interact with code-generating models. Proc. ACM Program. Lang. 7(OOPSLA1), 85–111 (2023)CrossRef

Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41–48 (2011)CrossRef

Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48119-2_22CrossRef

Berry, G.: Synchronous design and verification of critical embedded systems using SCADE and Esterel. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, p. 2. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-79707-4_2CrossRef

Bettini, L.: Implementing Domain-Specific Languages with Xtext and Xtend. Packt Publishing Ltd., Birmingham (2016)

Bitter, R., Mohiuddin, T., Nawrocki, M.: LabVIEW: Advanced Programming Techniques. CRC Press, Boca Raton (2006)

10.

Buck, J.T., Ha, S., Lee, E.A., Messerschmitt, D.G.: Ptolemy: a framework for simulating and prototyping heterogenous systems. Int. J. Comput. Simul. 4(2) (1994)

11.

Butler, R.W.: What is formal methods? NASA LaRC Formal Methods Program (2001)

12.

Campagne, F.: The MPS Language Workbench: Volume I, vol. 1. Fabien Campagne (2014)

13.

Chouali, S., Boukerche, A., Mostefaoui, A., Merzoug, M.A.: Ensuring the compatibility of autonomous electric vehicles components through a formal approach based on interaction protocols. IEEE Trans. Veh. Technol. 72(2), 1530–1544 (2023)CrossRef

14.

Cimatti, A., et al.: EVA: a tool for the compositional verification of AUTOSAR models. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 3–10. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-30820-8_1CrossRef

15.

Cocotec.io: Cocotec: All systems go. https://cocotec.io/

16.

Colón, M.A.: Schema-guided synthesis of imperative programs by constraint solving. In: Etalle, S. (ed.) LOPSTR 2004. LNCS, vol. 3573, pp. 166–181. Springer, Heidelberg (2005). https://doi.org/10.1007/11506676_11CrossRef

17.

Criado, J., Asensio, J.A., Padilla, N., Iribarne, L.: Integrating cyber-physical systems in a component-based approach for smart homes. Sensors 18(7), 2156 (2018)CrossRef

18.

Dajani-Brown, S., Cofer, D., Bouali, A.: Formal verification of an avionics sensor voter using SCADE. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 5–20. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_3CrossRef

19.

Simulation and model-based design (2020). https://www.mathworks.com/products/simulink.html

20.

Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL - An Introduction to the SAE Architecture Analysis and Design Language. SEI Series in Software Engineering. Addison-Wesley (2012)

21.

Fürst, S., Bechter, M.: Autosar for connected and autonomous vehicles: the autosar adaptive platform. In: Proceedings of DSN-w 2016, pp. 215–217. IEEE (2016)

22.

De Giacomo, G., Lenzerini, M., Leotta, F., Mecella, M.: From component-based architectures to microservices: a 25-years-long journey in designing and realizing service-based systems. In: Aiello, M., Bouguettaya, A., Tamburri, D.A., van den Heuvel, W.-J. (eds.) Next-Gen Digital Services. A Retrospective and Roadmap for Service Computing of the Future. LNCS, vol. 12521, pp. 3–15. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-73203-5_1CrossRef

23.

Jifeng, H., Li, X., Liu, Z.: Component-based software engineering. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 70–95. Springer, Heidelberg (2005). https://doi.org/10.1007/11560647_5CrossRef

24.

Hendriks, D., Aslam, K.: A systematic approach for interfacing component-based software with an active automata learning tool. In: Margaria, T., Steffen, B. (eds.) ISoLA 2022. LNCS, vol. 13702, pp. 216–236. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-19756-7_13CrossRef

25.

Hu, Y., Jiang, H., Tang, H., Lin, X., Hu, Z.: SQL#: a language for maintainable and debuggable database queries. Int. J. Softw. Eng. Knowl. Eng. 33(5), 619–649 (2023)CrossRef

26.

Kiss, T., Janosi-Rancz, K.T.: Developing railway interlocking systems with session types and Event-B. In: 11th IEEE International Symposium on Applied Computational Intelligence and Informatics, SACI 2016, Timisoara, Romania, 12–14 May 2016, pp. 93–98. IEEE (2016)

27.

Li, Y., Sun, M.: Component-based modeling in mediator. In: Proença, J., Lumpe, M. (eds.) FACS 2017. LNCS, vol. 10487, pp. 1–19. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68034-7_1CrossRef

28.

Liu, C., Yu, Q., Zhang, T., Guo, Z.: Component-based cloud computing service architecture for measurement system. In: 2013 IEEE International Conference on Green Computing and Communications (GreenCom) and IEEE Internet of Things (iThings) and IEEE Cyber, Physical and Social Computing (CPSCom), Beijing, China, 20–23 August 2013, pp. 1650–1655. IEEE (2013)

29.

McNutt, A.M.: No grammar to rule them all: a survey of JSON-style DSLs for visualization. IEEE Trans. Vis. Comput. Graph. 29(1), 160–170 (2023)

30.

Miranda, B., Masini, H., Reis, R.: Using simulink design verifier for automatic generation of requirements-based tests. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 601–604. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19249-9_42CrossRef

31.

Pearce, H., Tan, B., Krishnamurthy, P., Khorrami, F., Karri, R., Dolan-Gavitt, B.: Pop quiz! can a large language model help with reverse engineering? CoRR abs/2202.01142 (2022). https://arxiv.org/abs/2202.01142

32.

Salunkhe, S., Berglehner, R., Rasheeq, A.: Automatic transformation of SysML model to event-B model for railway CCS application. In: Raschke, A., Méry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 143–149. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-77543-8_14CrossRef

33.

Sanchez, L., Groote, J.F., Schiffelers, R.R.H.: Active learning of industrial software with data. In: Hojjat, H., Massink, M. (eds.) FSEN 2019. LNCS, vol. 11761, pp. 95–110. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31517-7_7CrossRef

34.

van der Sanden, B., et al.: Compositional specification of functionality and timing of manufacturing systems. In: Drechsler, R., Wille, R. (eds.) Proceedings of FDL 2016, pp. 1–8. IEEE (2016)

35.

van der Sanden, B., Blankenstein, Y., Schiffelers, R.R.H., Voeten, J.: LSAT: specification and analysis of product logistics in flexible manufacturing systems. In: Proceedings of CASE 2021, pp. 1–8. IEEE (2021)

36.

van der Sanden, B., Geilen, M., Reniers, M.A., Basten, T.: Partial-order reduction for supervisory controller synthesis. IEEE Trans. Autom. Control 67(2), 870–885 (2022)MathSciNetCrossRef

37.

Sifakis, J.: Component-based construction of real-time systems in BIP. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 33–34. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_4CrossRef

38.

Ströder, T.: Symbolic execution and program synthesis: a general methodology for software verification. Ph.D. thesis, RWTH Aachen University, Germany (2019)

39.

Szyperski, C., Gruntz, D., Murer, S.: Component Software – Beyond Object-Oriented Programming, 2nd edn. Publishing House of Electronics Industry (2003)

40.

Touvron, H., et al.: Llama 2: open foundation and fine-tuned chat models. CoRR abs/2307.09288 (2023). https://doi.org/10.48550/arXiv.2307.09288

41.

Trivedi, P., Zulkernine, F.H.: Componentry analysis of intelligent transportation systems in smart cities towards a connected future. In: 22nd IEEE International Conference on High Performance Computing and Communications; 18th IEEE International Conference on Smart City; 6th IEEE International Conference on Data Science and Systems, HPCC/SmartCity/DSS 2020, Yanuca Island, Cuvu, Fiji, 14–16 December 2020, pp. 1073–1079. IEEE (2020)

42.

Ait Wakrime, A., Ben Ayed, R., Collart-Dutilleul, S., Ledru, Y., Idani, A.: Formalizing railway signaling system ERTMS/ETCS using UML/Event-B. In: Abdelwahed, E.H., Bellatreche, L., Golfarelli, M., Méry, D., Ordonez, C. (eds.) MEDI 2018. LNCS, vol. 11163, pp. 321–330. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00856-7_21CrossRef

43.

Whitten, J.L., Bentley, L.D., Ho, T.I.: Systems Analysis & Design Methods. Times Mirror/Mosby College Publishing (1986)

44.

Yang, M., Zhang, D.: Deep reinforcement learning guided decision tree learning for program synthesis. In: Zhang, T., Xia, X., Novielli, N. (eds.) IEEE International Conference on Software Analysis, Evolution and Reengineering, SANER 2023, Taipa, Macao, 21–24 March 2023, pp. 925–932. IEEE (2023)

45.

Yang, N., Cuijpers, P.J.L., Schiffelers, R.R.H., Lukkien, J., Serebrenik, A.: Single-state state machines in model-driven software engineering: an exploratory study. Empir. Softw. Eng. 26(6), 124 (2021)CrossRef

46.

Zhao, W.X., et al.: A survey of large language models. CoRR abs/2303.18223 (2023)

47.

Zheng, Z., Tian, J., Zhao, T.: Refining operation guidelines with model-checking-aided FRAM to improve manufacturing processes: a case study for aeroengine blade forging. Cogn. Technol. Work 18(4), 777–791 (2016)CrossRef

Title: Challenges Engaging Formal CBSE in Industrial Applications
Authors: Yi Li
Meng Sun
Publisher: Springer Nature Switzerland
Book: Formal Aspects of Component Software
Print ISBN: 978-3-031-52182-9

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

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

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner