A service-oriented methodology supporting automatic synthesis and verification of component behavior model

It is very difficult to construct correct component behavior models for distributed, reactive system. The concept of service makes us revisit the method of how to construct component behavior models. On the contrary, current descriptions of service are mainly based on syntax. Because service lacks of a systematic semantic description, it is hard to develop service with high quality and reliability. In this paper we combine the ideas of service and component; propose a new methodology supporting automatic synthesis and verification of component behavior model. This method uses traditional scenario-based synthesis technique to synthesize each role behavior model of service, and verifies desired properties of role by model checking, then synthesizes component behavior model by composing all roles participated in different services, and verifies liveness properties of component by compositional reasoning thus avoids searching the whole state space of component.