The Java programming language supports component based software development through JavaBeans. JavaBeans are Java components. The JavaBeans specification document uses a natural language and informal diagrams. It is common to interpret natural language in a number of ways which is exactly the problem in the requirement analysis phase of a software development life-cycle. As there are no separate syntactical rules and kewords for JavaBeans an application of formal techniques is required to create a rigorous specification document. This report presents a formal model of JavaBeans and refines the model towards implememtation. In our model, we use predicative logic to express JavaBeans unambigiously. The goal of the abstract formalisms is to divide a system into a number of interconnected JavaBeans. This allows developers to improve the system performance by reorganizing its constituent components. A notion of refinement has been adopted to formalize the replaceability of JavaBeans. The goal of the refinement and implementation level formalisms is to develop a mathematical characterization of JavaBeans that is close to Java features which can be used to specify, refine and implement JavaBeans. The case study shows a typical course that can be taken from the abstract model to implementation oriented formalisms.
