A Case Study of Choreography Realizability Checking on Smart Home Application

This paper studies the choreography realization problem that is a problem to synthesize a concrete model from an abstract specification in service-oriented architecture. So far, we have studied the problem on a case where the choreography was defined by one or two scenarios and was expressed by an acyclic relation of events. In our previous study, we proposed the use of event structures to express choreography. In addition, we introduced the re-constructibility of event structures, which is a property of them to be satisfied, and showed a necessary condition for an event structure to be re-constructible. In this paper, we use a simple example of a smart home where the choreography is defined by three scenarios with multiple message sets. We demonstrate the re-constructibility of the event structure created from the choreography.