Animation-Based Service Specification, Verification and Validation

[Context] With the expansion of services and service science, service systems have become an important abstraction for the service revolution. Service is defined as the application of resources (including competences, skills, and knowledge) to make changes that have value for another (system). The service system is a configuration of people, technologies, and other resources that interact with other service systems to create mutual value. Many systems can be viewed as service systems, including families, cities, and companies, among many others. Therefore, services became very important for unifying concepts from various disciplines. Service specifications are used to represent service systems on different levels of abstraction: from business down to IT. [Motivation and Problem] Traditionally, high-level service specifications are used only for communication among different participants, to catalyze the discussions between them; but only the specifications modeling IT systems have enough details to be simulated and executed. As a consequence, it becomes difficult to create precise high-level specifications and make sure that the implemented services are those that correspond to the business needs, potentially leading to severe project problems. Therefore, the challenge is to create abstract, yet precise service specifications, while keeping the relation between specifications at different levels of abstraction. [Idea and Results] In this work, we use formal methods and code generation techniques to create service-prototypes from service specifications at any level of abstraction, keeping the relations between different specifications. Stakeholders can try out the prototypes and give feedback regarding services that are being provided. This way, prototypes are used to validate the specifications and detect inconsistencies and unexpected behavior. [Contribution] The contributions of our work are threefold. First, we provide the visual formalism for service specification and simulation, by adding the necessary concepts to the existing method SEAM. Second, we define two design spirals: for service specification and for service validation and verification. The service specification spiral enables us to keep the relation between several service specifications. It includes steps with explicit design decisions on how to refine high-level specifications in order to include all the details necessary for providing the identified services. The validation and verification spiral is used to validate and verify specifications at any level of abstraction. Finally, it provides an environment that enables the simulation and prototyping of service specifications that are then used for their validation and verification. [Relevance] In addition to the theoretical contribution to the knowledge base of service design, we also provide the tools and guidelines that help business and IT analysts create and validate the service model, as confirmed by a survey conducted with practitioners. We illustrate the application of this work with a case study based on a consulting project we conducted at EPFL.