Service-oriented modeling using the SOFL formal engineering method

Service-oriented computing advocates the development of new software or services on the basis of existing services. This paradigm shows a great potential of achieving high productivity and low cost, but it faces a challenge in efficiently and correctly using existing services in producing a new application and ensuring its reliability. Building a formal model using a formal specification language allows the developer to thoroughly understand what existing services are needed for the new application, but how to construct the model so that it can effectively facilitate the developer to recognize the appropriate services still remains an open problem. In this paper, we describe an approach to applying the SOFL formal engineering method to the modeling of a service-oriented system by means of a case study. In particular, we focus on the issue of how to apply the SOFL three-step modeling approach to the construction of a formal specification for a service-based system, exploring the general principle and specific techniques for reusing existing services in developing a system model.