Validation of Component based Software Development Model using Formal B-Method

IT industry in the present market situation faces high demand for performance and burgeoning user expectations; with the pressure manifesting itself in three forms - Development Cost, Time-to-market and Product Quality. One of the relevant techniques in this context is Component Based Software Development (CBSD) with a targeted and discriminative approach influencing all phases of development. Although this approach offers great benefits of reusing ready- made components such as reducing time-to-market products and development costs, it also poses serious questions on the correctness of created systems. In this paper a methodology is proposed using a formal B-method approach, which supports formal stepwise development with refinement to model component-based systems in view of interaction among components. The proposed methodology is illustrated by a case study; Atelier B. is used to generate proof obligations and executable code automatically.