Service Oriented Product Line: Analysis and Verification

Abstract

In computer science and software engineering, re-usability is the use of existing assets in some form within the software product development process. A software product line (SPL) is a set of software-intensive systems that share a common, managed set of features satisfying the specific needs of a particular market segment or mission and that are developed from a common set of core assets in a prescribed way. A service-oriented architecture is essentially a collection of services. These services communicate with each other. The communication can involve either simple data passing or it could involve two or more services coordinating some activity. Some means of connecting services to each other is needed. Web Service technology provides a platform on which we can develop distributed services. The interoperability among these services is achieved by various standard protocols. Web service composition originated from the necessity to achieve a predetermined goal that cannot be realized by a standalone service. Internally, in a composition, services can interact with each other to exchange parameters, for example a service's result could be another service's input parameter. We need verification of service composition to check whether there is any errors/deadlock in the composite service and are there any difficulties in the composite service? There are two types of service composition and we focused only on service choreography. To verify the service composition we used process algebraic technique, FPS. We model the service choreography in FSP and then use LTSA tool to animate the transitions and verify the composition.