Challenges Engaging Formal CBSE in Industrial Applications

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.