Component contract-based formal specification technique

When we analyze the business domain, we have to decide what business concepts are to be encapsulated into a component and find what business concepts are to be built by using a reuse component. Also, as a component is reused in the form of a black-box, the reuser must have detailed information about the component, such as the functional and non-functional performance which is necessary to reuse or integrate. So, we will propose a formal approach to design a robust component. First, we analyze a business domain by using Z and category theory. Second, we extract the components and the interfaces from previous analysis results. Lastly, we add component contracts(functional and non-functional performances) to the result. We specify business concept based on DbC which is used broadly to specify the behavior of an interface in an object-oriented area. Also, we will define rules for extraction of components and component contracts from specification. Specially, we will use category theory to analyze the relations between components.