IWSN: A novel method for modeling the interaction of web services

Abstract

As the most notable implementation of service-oriented architectures, web services has brought some challenging research issues, one of which is the composition. Correct interaction among web services is the prerequisite of their successful composition. In this paper, we propose a novel approach to model dynamic interactive behavior of web services, aiming to effectively take advantage of the flexibility of service composition technology and guarantee the behavior compatibility of web services and further to facilitate the application of web service composition in healthcare field. An interaction model of web services based on Kahn process network (KPN) is presented in this paper, which is a data-flow and channel-based model supporting parallel and cooperative computation. Formal behavioral semantics of this model is defined by Pi-calculus process algebra and formal properties of the proposed model are discussed. An application case is demonstrated to illustrate how the proposed model can be applied to describe services behavior and their interaction. The reachability analysis of the application case is performed based on modal -calculus. How the supporting tool, i.e. CWB-NC, can be utilized to verify the properties we anticipate is presented.

Keywords

Web service Pi-calculus process algebra KPN service interaction

1. Introduction

With the transfer of diet, lifestyle and working way in recent years, the number of patients with chronic diseases continues to increase worldwide. Various health risks that people are facing with grow with each passing day. With this background comes the urgent need for health supplemented software. As an important technology that is usually used in supporting cloud computing [1, 2], Web Services (WSs) can be used to collect, store and analyze health-related data from various information networks and terminal technologies, and thus implementing the functions of health monitoring and management, physical health prediction, healthy lifestyle consultation, doctor-patient information interaction and knowledge learning.

Figure 1.

The web service composition of diabetic information consultation.

Health supplemented software have such feature that it usually needs the support of multiple service software which collect different kinds of data to accomplish the assessment of the relevant health condition. To roughly predict blood glucose, for instance, we need at least patient’s BMI, patient’s insulin dosage, patient’s calorie intake, patient’s amount of exercise that can used to assess patient’s energy consumption. Obviously, single software service, such as step counting software (a software used to estimate the calories we consume daily), can not realize the functionality we desired. To address this issue, we need a method that can integrate the functions of software services.

Service composition techniques [3, 4] provide ways to devise a composition of software services, which can fulfill aforementioned requirement. The advantage of SOA [5] is it can integrate a wide array of existing services that are interoperable to each other to form a composite service. Service designers could devise a composite business process that makes the best use of existing services, providing a way to glue all component services together with least augmentation or modification. There are a number of studies on automatic web service composition, but there is not much on applying service composition technology to solve healthcare related issues.

The remainder of this paper is organized as follows: A motivating example is presented in Section 2. Research challenges and background and related works are introduced in Section 3 and Section 4 respectively. Section 5 presents our service interaction model: Interactive Web Service Network. Section 6 provides the behavior semantics of Interactive Web Service Network. Section 7 provides a case study. Conclusions and future works are drawn in Section 8.

2. Service composition in healthcare field: A motivating example

To illustrate the importance of behavioral compatibility in Web Service composition, which motivates our work, we present a software service example of information consulting on the condition of blood glucose for diabetic patients.

If we want to, for instance, assist diabetic patients with information consultation so as to help control their postprandial blood glucose, which will play a active role in slowing the progression of diabetes. There are many factors that will influence the postprandial blood glucose of diabetic patients. Such common factors as insulin dosage, calorie intake per meal, daily exercise, etc all possibly affect the postprandial blood glucose. These basic data are needed if we want to predict postprandial blood glucose in diabetic patients. Common software services that can be used to collect the relative data are the Step Counting Service, Caloric Intake Recording Service, Data Analysis Service, etc. But apparently these services are all atomic services that cannot meet our demand. There is a need to compose the Blood Glucose Control Consulting Service, which is responsible for answering the questions from patients and providing advises, the Step Counting Service that is responsible for recording the calories patients burned, the Caloric Intake Recording Service that is responsible for recording the calories patients intake, and the Data Analysis Service that is responsible for processing and analyzing the data. The web service composition that are composed of these services, as illustrated in Fig. 1, will accomplish the information consultation about the condition of the blood glucose in diabetic patients.

Figure 2.

State transition graph of the participating services.

3. Research challenges and our contributions

Some challenges face the successful composition process of web services, one of them is the services behavior compatibility. We will briefly present the compatibility issues in the following simple scenario. In order to provide the users with the analysis results of blood glucose data, the Blood Glucose Control Consulting Service needs to interact simply with the Data Analysis Service. The behavior of these two services is illustrated in Fig. 2. Meanings of elementary graphical structures in Fig. 2 is introduced as follows:

•
denotes the sequential structure, which indicates that the states transition from $S1$ to $S2$ through action $A1$ ;
•
denotes the parallel structure, which indicates that service transits into states Sp1 and SC1 in parallel from state S1, after executing action A1, i.e. when states $S_{p1}$ , $S_{c1}$ transit to their respective subsequent states, they are not mutually affected by each other.

The workflow of the Blood Glucose Control Consulting Service is briefly introduced as follows: as illustrated in Fig. 2, the initial state of Blood Glucose Control Consulting Service is $S1$ . It will first invoke the Data Analysis Service, requesting the analysis results of relevant blood glucose data (denoted by action A1) and transits into state S2. Then it will receive the analysis results from the Analysis Service (denoted by action A2) and transits into state S3, its terminate state. The outline of the workflow of the Data Analysis Service is as follows: it is first invoked by request from the Consulting Service, which requires to obtain the analysis results of blood glucose data (denoted by action A1). Then, in order to retrieving the relevant data needed for analysis, it will invoke other services (for example, Step Counting Service and Caloric Intake Recording Service) and receives data from them in parallel (denoted by actions A2, A3). Finally it will provide the Consulting Service with the required the analysis results(denoted by action A4) and transits to its terminate state. Behavior compatibility can be intuitively understood as a kind of binary relation over the set of actions in the structural execution sequences. For example, tuples ( $A_{c1}$ , $A_{d1}$ ) and ( $A_{c2}$ , $A_{d5}$ ), as illustrated with the rectangles that are connected by the dotted lines in Fig. 2. The scenario describe above belongs to the situation of behavior compatibility and we will give a formal definition for behavior compatibility in Section 6.

We proposes a novel process network approach for modeling the interactive behavior of web services, aiming to verify the behavior compatibility of web services. A mathematical base for behavior compatibility is established by giving its formal definition, implying the service behavior represented in this model can be analyzed and verified using verification tools like CWB-NC [6].
4. Research background and related works

As briefly mentioned in Section 3, to address the issue of behavior compatibility an effective way is to formalize the interactive behavior of services such that this problem will be transformed into a mathematical one. This section aims at giving a detailed introduction to formal method related to web service interaction and providing a brief review of existing relevant approaches. Various technologies, approaches, and frameworks for web service interaction and their application have been explored recently.

4.1 Petri nets based approaches

Because of the formally semantics defined of Petri nets, by mapping each web service to a Petri net a formal model of web service can be obtained, in which case the verification techniques and tools can be utilized. Since Petri nets are graphical languages, one major disadvantage of the Petri-nets based methods is the number of the places and the transitions defined by them may be too large. In many cases researchers map each element in a web service composition language to an element in a Petri net and do not limit its the number of the places and the transitions, in which case a condition of state explosion may happen.

Researchers presented a Petri nets-based formal model for Web service interaction [7]. They model the basic activities, structured activities, and interfaces among BPEL processes by utilizing the elements in Petri-net that correspond to them. Researchers analyze the model using structural properties instead of reachable states and add constrains to their model to prevent from reaching incompatible states. To guarantee the compatibility automatically, their model can be transformed back to code in BPEL by reducing the need to search other replaceable web services.

To analyze timed compatibility among web service composition, a model called divide-and-conquer based on Petri nets is presented in [8]. Researchers generate a timed state graph in a modular approach first before checking the temporal violations in the service composition. A mediation net is used in composing the services to avoid message mismatching. Researchers also give a method that aims to generate reliable and usable execution paths for the participating services, which will help direct customers to successfully execute service composition.

Researchers model such interactive systems as Web services and workflows with the help of Petri nets [9]. In their work the definition of compatibility and weak compatibility for Interactive Petri Nets (IPNs in short) is given, the relationships among properties like boundedness, compatibility and liveness is presented, and the inference that the compatibility analysis belongs to co-NP-hard problem is proved. IPNs classification and structure-based method are used to analyze and explore the properties of IPNs such as liveness and (weak) compatibility.

A bottom-up approach to built service composition that could give a concise representation of service composition is presented in [10]. In their work, service operation are modeled as transitions with input/output places and the input/output messages of operations are modeled as colored places. An element called Service Net (SN in short) that includes all operations required by service composition is generated first, and then a kind of decomposition techniques based on Petri nets are used to derive a subnet from this element, which will meets the need of the business requirement.Their approach can also be used to decompose service composition from top to bottom that will export candidate solutions with required structure. One merit of their method is when new services are added or deleted the service composition can be modified incrementally, which means service composition does not need to be built from the scratch.

Researchers propose a method selecting web services through an application called composition manager, which chooses services according to their quality and transaction behavior [11]. This method free the customers to focus on the construction of the desired functionalities. A selection algorithm utilizing patterns of workflow and transaction information of the component services is given and evaluated. By means of matching the properties of web services with the user’s desires, researchers give the indicators that indicates whether the results can be compensated or not. The criterion applied in selecting web services is the transactional and QoS properties of services required by users, which are expressed as weights over each QoS dimension.

4.2 Process algebra based approaches

Process algebra is a kind of concurrent language which abstracts from many details and concentrates on describing the services’ exterior behavior and this feature make it suitable to verify the interaction correctness among web services. However, some kinds of complex structures in web service composition can not be described using the process algebra based methods. Another difficulty involved in using these methods is the establishment of a rigorous translation mechanism, which translates descriptions of web service composition into expressions of process algebra.

Zhang et al. [12] propose an interaction model of context-aware web services based on Context-aware Process Network (CAPN). In their work the CCS process algebra based behavioral semantics for this model is defined and the method to implement context awareness and behavior adaptation of web services is discussed too.

To guarantee the validity of web services composition, Liao et al. apply Pi-calculus to model web services composition [13]. The differences between Pi-calculus and other process algebra based formal methods is discussed, rules for translating form web services into Pi-calculus is presented and the method of modeling agents and channels used in web service composition is explained in their work.

To verify the correctness of web service composition and enhance their reliability, a Pi-Calculus based formal method for describing and verifying web services composition is presented in [14]. Researchers also demonstrate the application of the proposed method through the modeling process of an online movie ticket booking system and formally analyze and verified the properties of this system with the help of mobility workbench (MWB in short), a verification tool developed for Pi-calculus.

5. Interactive web service network: A service interaction model

To describe the interactive behavior of web services at the message level, we define an interaction model of web services, which is named as Interactive Web Service Network (IWSN in short), whose design idea comes from a data-flow and channel-based model of cooperative computation, i.e., Kahn process network (KPN in short) [15]. A brief introduction of KPN is presented in the following paragraph.

5.1 Kahn process network

Kahn process network (KPN) is a data-flow based model of computation and has been used for modeling the interactive behavior of web services [12]. A advantage of KPN that makes it very suitable applied here is it can implement parallel communication and execution of processes on a distributed structure. In KPN model, concurrent processes is denoted as nodes, and ordered sequences of data is represented as arcs which is also called tokens in KPN. Concurrent processes communicate with each other by means of First-In-First-Out channels, which are denoted as queues of data tokens. Read actions from the FIFO channel can not initiate until at least one token becomes available. Since the sizes of FIFO channels are unbounded, writing actions are non-blocking. A token can only be read once from FIFO. When an input arrives, the output result of KPN’s computation is independent of its execution order and this property is consistent with that of our model which we will explain in the following chapters. The communication mechanism for KPN is asynchronous.

5.2 Interactive web service network

Interactive Web Service Network model the web service interaction as a concurrent autonomous network of processes. A web service is modeled as a computing process in KPN. Processes communicate with each other through First-In-First-Out channels. Each process in network has its own control over the sequences of messages, and each process performs its operations concurrently with other services. For individual processes (services), its behavior represents its execution operations. Trace is used to describe and record the interaction behavior among processes. IWSN is illustrated in Fig. 3.

Figure 3.

Interactive web service network.

5.3 Formal definition of interactive web service network

The elementary functional unit for a web service is operation. Web service invocations can be modeled as processes of invocation operations. In IWSN, the invocation of operation is modeled by Operation. For accurately describing the structure of operation executions, we introduce a set of processes, i.e. Process, as the elementary control unit. A process in Process is a linear concatenation of operations. If the output message of one operation op ${}_{1}$ is the input message of another operation op ${}_{2}$ , then there exists some corresponding relation between op1 and op2, herein a binary relation $R_{o}$ is introduced to represent this type of relation. Symbol $T$ is introduced in IWSN to denote the interaction history of processes (web services).

Definition 1 (Interactive Web Service Network). An Interactive Web Service Network is a septuple $<$ Service, Process, Operation, $T$ , Message, $R_{o}$ , $M$ $>$ , where:

•
Service is a set of web services;
•
Process denotes a set of processes;
•
Operation denotes a set of operations;
•
$T$ denotes a set of sequences of operations;
•
Message denotes a set of messages transmitted to and from processes;
•
$R_{o}\subseteq$ Operation $\times$ Operation is a binary relation over the set of Operation;
•
$M$ is a sextuple $<f_{pt}$ , $f_{ps}$ , $f_{pu}$ , $f_{op}$ , $f_{ot}$ , $f_{mo}>$ , where:

–
$f_{pt}$ : Process $\to$ {composite, elementary} is a mapping that indicates the type of a process;
–
$f_{ps}$ : Process $\to$ Service is a mapping that associate a process with a service;
–
$f_{pu}$ : Process $\to$ Process is a mapping that associate a elementary process with a composite process;
–
$f_{op}$ : Operation $\to$ Process is a mapping that associate a operation with a process;
–
$f_{ot}$ : Operation $\to$ {in-in, in-out, en-in, en-out, exe} is a mapping that indicates the type of operation (inner input, inner output, environment input, environment output, execute);
–
$f_{mo}$ : Message $\to$ Operation is a mapping that associates a message with an operation;

We let $f_{con}(p)={\{}o|o\in\textit{Operation}\wedge f_{op}(o)=p{\}}$ for $p\in\textit{Proc}\wedge f_{pt}(p)=\textit{elementary}$ ; Let $<_{o}\subseteq$ Operation $\times$ Operation be a partial order relation over the set of Operation, defined as: $<_{o}={\{}o_{1}$ , $o_{2}|o_{1}$ , $o_{2}\in\textit{Operation}\wedge f_{op}(o_{1})=f_{op}(o_{2})\wedge o_{1}$ happens earlier than $o_{2}$ }. An element $p$ in Process is constructed according to the following grammar:

$\displaystyle p=o|\textit{proc}_{1}||\textit{proc}_{2}|\textit{proc}_{1}<_{o}% \textit{proc}_{2}$ (1)

where: $o\in\textit{Operation; proc}_{1}$ , $\textit{proc}_{2}\in\textit{Process};\textit{proc}_{1}||\textit{proc}_{2}$ is a new process that performs $\textit{proc}_{1}$ and $\textit{proc}_{2}$ in parallel and $\textit{proc}_{1}<_{o}\textit{proc}_{2}$ is a new process that perform $\textit{proc}_{1}$ and $\textit{proc}_{2}$ sequentially.
6. Behavior semantics of interactive web service network

The behavior semantics of Interactive Web Service Network is defined in this section that is based on Pi-calculus and its axiomatic operational semantics [16]. The behavior semantics consist of two parts: semantic range and valuation functions. Pi-calculus is introduced as a semantic range, and then valuation functions are defined to translate an IWSN (semantic domain) instance into expressions in Pi-calculus.

As the development of Calculus of Communication System (CCS in short) [17, 18], Pi-calculus unify such objects as variable, names and channel names in CCS and dose not differentiate them. Pi-calculus is capable of modeling new channels due to its features like transferring not only the variables and names in CCS but also the channel names, which makes Pi-calculus suitable to describe the concurrent system with changing structure.

6.1 Syntax of Pi-calculus

In Pi-calculus processes are denoted by capital letters $P$ , $Q$ , $R\ldots$ , which are the elements in a countable infinite set of names $N$ and actions performed by these processes are represented by lowercases $u$ , $v$ , $w$ , $x$ , $y$ , $z\ldots$ , which are the elements of $N$ . Pi-calculus expressions are constructed with the following grammar:

$\displaystyle P::=0\left|\sum P_{i}\right|cx.P|(P_{1}|\ldots|P_{n})|_{[x=y]^{P}}$ (2)

A null process written as 0, meaning this process terminates; symbol $\sum$ donotes the non-deterministic choice, e.g., $R^{+}P$ expression means performing $R$ or $P,$ but not both; A sequential execution written in the form cx. $P$ , where $P$ is a process, $c$ is a channel name and $x$ is an action name, means input $x$ from $c$ and then execute $R$ ; expression $Q+P$ denotes a non-deterministic choice, meaning executes processes $P$ or $Q$ , but not both. Parallel execution denoted as $P_{1}|\ldots|P_{n}$ , which means the parallel composition of processes $P_{1}$ , $P_{2}$ , $\ldots$ , $P_{n}$ . Process written as ${}_{[x=y]}{}^{P}$ means when channel name $x$ equals channel name $y$ , process ${}_{[x=y]}{}^{P}$ behaves the same as $P$ does, otherwise, it is a null process. In Pi-calculus symbol $\tau$ represents hidden actions performed by two synchronized sub-processes, which are invisible to outside observers.

6.2 Operational semantics of Pi-calculus

The operational and axiomatic semantics of Pi-calculus determine the possible derivations of a process, which establish the formal foundation for Pi-calculus. The inference rules are presented in Table 1:

Table 1
The inference rules of Pi-calculus

Empty Action: $\overline{\tau.P\buildrel\tau\over{\longrightarrow}P}$ , where $\tau$ represents empty action and $P$ represents a process;	(3)
Output Action: $\overline{\mathop{x}\limits^{-}y.P\mathop{\to}\limits^{\mathop{x}\limits^{-}y}P}$ , where $x$ , $y$ represent actions and $P$ represents a process;	(4)
Input Action: $\overline{x\,(z).P\mathop{\to}\limits^{x(y)}P\{y/z\}}$ , $y\notin f_{n}\,(z.P)$ , where $x$ , $y$ , $z$ represent actions, $P$ represents process and $f_{n}$ represents replacing function;	(5)
Branch: $\frac{P\mathop{\to}\limits^{a}P^{\prime}}{P+Q\mathop{\to}\limits^{a}P^{\prime}}$ , where $a$ represent action and $P$ , $Q$ represent processes;	(6)
Parallel: $\frac{P\mathop{\to}\limits^{a}P^{\prime}}{P\|Q\mathop{\to}\limits^{a}P^{\prime}% \|Q}$ , where $a$ represents action and $P$ , $Q$ represents processes.	(7)

6.3 Valuation functions

The valuation functions for IWSN and their the semantic domain and semantic range are given in Table 2, in which Proc denotes process expression in Pi-calculus, $E$ denotes a set of elementary processes, Opr denotes a set of operations and Act denotes a set of Actions in Pi-calculus.

Table 2
Valuation functions for IWSN

Valuation functions	Domain	Range
$f_{n}$	IWSN	Proc
$f_{d}$	Process	Proc
$f_{b}$	Process	Proc
$f_{s}$	$E$	Proc
$f_{f}$	Opr	Act

Valuation functions are defined as follows:

$\displaystyle f_{n}(s_{r})=f_{c}(s_{1})|f_{c}(s_{2})|\ldots|f_{c}(s_{n}),\text% {where:}$ (8) $\displaystyle\quad s_{r},s_{i}\in\ \text{Service}\ (1\leqslant i\leqslant n)\ % \text{and}\ f_{s}(s_{r})=\emptyset\wedge f_{s}(s_{i})=s_{r};$ $\displaystyle f_{d}(s_{i})=f_{b}(s_{i})\ \textit{iff}\ f_{pt}(s_{i})=e;$ (9) $\displaystyle f_{d}(s_{i})=f_{r}(s_{i})\ \textit{iff}\ f_{pt}(s_{i})=c;$ (10)

$\displaystyle f_{b}(s_{i})=f_{f}(a_{1})\cdot f_{f}(a_{2})\ldots f_{f}(a_{n}),% \text{where:}$ (11) $\displaystyle\quad a_{i}\in_{Opr}\wedge f_{f}(a_{i})=s_{i}\ \text{and}\ a_{1}<% _{o}a_{2}<_{o}\ldots<_{o}a_{n};$ $\displaystyle f_{f}(a_{i})=a_{i}\ \textit{iff}\ f_{ot}(a_{i})=\textit{ in-in}% \vee\textit{en-in};$ (12) $\displaystyle f_{f}(a_{i})=a_{i}\ \textit{iff}\ f_{ot}(a_{i})=\textit{ in-out}% \vee\textit{en-out};$ (13) $\displaystyle f_{s}(s_{i})=f_{d}(s_{1})|f_{d}(s_{2})\ \textit{iff}\$ (14) $\displaystyle\quad f_{pu}(s_{1})=s_{i}\wedge f_{pu}(s_{2})=s_{i}\wedge s_{i}=s% _{1}||s_{2};$ $\displaystyle f_{s}(s_{i})=f_{d}(s_{1}).f_{d}(s_{2})\ \textit{iff}$ (15) $\displaystyle\quad f_{pu}(s_{1})=s_{i}\wedge f_{pu}(s_{2})=s_{i}\wedge s_{i}=s% _{1}<_{o}s_{2.}$

An algorithm aiming at translating an IWSN instance to Pi-calculus expressions are presented as follows on the basis of the valuation functions defined in Algorithm 1:

Algorithm 1. IWSN Translation
INPUT: IWSN Instance
OUTPUT: The translated Pi-calculus expressions
Step 1: Proc Translate_ $f_{n}$ (IWSN Instance)
{ String e $=$ Null;
For every $p$ in Process: e $=$ e $\|$ Translate_ $f_{d}$ (proc);
Return e; }
Step 2: Proc Translate_ $f_{d}$ (for proc $p$ in Process)
{ If (process Type $=$ elementary) Return Translate_ $f_{b}(p)$ ;
Else Return Translate_ $f_{d}(p)$ ;}
Step 3: Proc Translate_ $f_{r}$ (for proc $p_{i}$ in Process)
{ String e $=$ Null;
For every sub-service $s_{j}$ of proc p ${}_{i}$
If (serviceType of $s_{j}=$ parallel) e $=$ e $\|$ Translate_ $f_{d}$ (s ${}_{j}$ );
Else e $=$ e. Translate_ $f_{d}$ ( $s_{j}$ );
Return e; }
Step 4: Proc Translate_ $f_{b}$ (for process p ${}_{i}$ in Process)
{ String name $=$ Null;
name $=$ get-name( $p_{i}$ );
For every opr $o_{i}$ in Operation of proc $p_{i}$
If (operationType $=$ output) name $=$ !get-name(o ${}_{i})$ . name;
Else If (operationType $=$ input ) name $=$ get-name( $o_{i}$ ). name;
RETURN name; }

6.4 Formal definition of behavior compatibility

Observational Equivalence needs to be defined ahead of the definition of Behavior Compatibility. The definition of observational equivalence lays the conceptual basis for deciding that whether the behavior of two web services can be considered to be the same. It can also be used in reducing verification work by replacing a process by a smaller (in size), but equivalent one.

Definition 2 (Weak Transitions).

$\textit{iff}\ q=q_{0}\to^{\tau}q_{1}\to^{\tau}\ldots\to^{\tau}q_{n}$ , then $q\Rightarrow^{\varepsilon}q^{\prime}$ , where $n\geqslant$ 0 and $\tau$ denotes a transition label for operation which is not externally visible;

$\textit{iff}\ q\Rightarrow^{\varepsilon}q^{\prime}$ , then $q\Rightarrow^{\tau}q^{\prime}$ ;

$\textit{iff}\ q\Rightarrow^{\varepsilon}q_{1}\to^{a}q_{2}\Rightarrow^{% \varepsilon}q^{\prime}$ , then $q\Rightarrow^{a}q^{\prime}(a\neq\tau)$

$\textit{iff}\ q\Rightarrow^{a}q^{\prime}$ , then the transition from $q$ to $q^{\prime}$ is a weak transition

Definition 3 (Observational Equivalence).

Let $R\subseteq$ Q $\times$ Q, then the relation R is a weak bisimulation iff

whenever $t_{1}$ Rt ${}_{2}$ then:

•
$t_{1}\to^{a}t_{1}^{\prime}$ means $t_{2}\Rightarrow^{a}t_{2}^{\prime}$ for some $t_{2}^{\prime}$ such that $t_{1}^{\prime}Rt_{2}^{\prime}$ ;
•
$t_{2}\to^{a}t_{2}^{\prime}$ means $t_{1}\Rightarrow^{a}t_{1}^{\prime}$ for some $t_{1}^{\prime}$ such that $t_{1}^{\prime}Rt_{2}^{\prime}$

If there is a weak bisimulation relation $R$ over $t_{1}$ and $t_{2}$ , i.e., $t_{1}Rt_{2}$ , then $t_{1}$ and $t_{2}$ are observationally equivalent, or weakly bisimulation equivalent.

Definition 4 (Behavior Compatibility). Two interacting web services $p$ and $q$ are behavior compatible, denoted as compatible ( $p$ , $q$ ), iff they have opposite behavior trace (only including reading/writing actions on FIFO channels between this two web services), i.e., $p$ is observationally equivalent to $q$ .

Definition 5 (Effectiveness). Let $\Sigma$ be a alphabet of channel names, an execution e of an IWSN with an input In is effective, denoted as effective (In), iff in the last configuration only read action are allowed and all inputs of input in: In $\to\Sigma$ * have been processed.

Theorem 1 (Deterministic). A IWSN Instance is determinate.

Proof. Using the histories of supply tunnels, which are the sequences of events and finite in length, to record mathematically the interaction of services, and Processes (Services) are discrete functions that operate on these sequences. In this way, we can present IWSN by a set of equations. The history of a supply tunnel is a finite sequence of events represented as $H_{e}=[e_{1},e_{2},\ldots,e_{n}]$ . An empty sequence is represented with the symbol $\Theta$ . Let $S_{h}$ represent the set of all such sequences. Consider there exists a prefix ordering over sequences, where the sequence $H_{e2}$ preceded by the sequence $H_{e1}$ (written as $H_{e1}\subseteq H_{e2})$ if $H_{e1}$ is a prefix of, or $H_{e1}$ is equal to, $H_{e2}$ . Empty sequence $\Theta$ is a prefix of all sequences.

Obviously, the relation $\subseteq$ defined above is transitive, antisymmetric and reflective, which means the relation $\subseteq$ gives us a partial order over set H. Given any finite increasing chain of sequences $[H_{e}]=(H_{e1},H_{e2},\ldots,H_{en})$ with $H_{e1}\subseteq H_{e2}\subseteq\ldots\subseteq H_{en}$ has a least upper bound $U_{[He]}=H_{en}$ such that $H_{ei}\subseteq U_{[He]}$ for all $H_{ei}\in[H_{e}]$ .

Since for every increasing sequence, there exists a least upper bound that is also in set [ $H_{e}$ ], then the relation $\subseteq$ defines a complete partial order over [ $H_{e}$ ]. In IMSN, an elementary process (service) can be modeled as a functional mapping operated on input and output sequences $f$ : [ $H_{e}$ ] $\to$ [ $H_{e}$ ]. Function $f$ maps an increasing sequence $[H_{e}]=(H_{e1},H_{e2},\ldots,H_{en})$ into another set of sequences $[H^{\prime}_{e}]=(H^{\prime}_{e1},H^{\prime}_{e2},\ldots,H^{\prime}_{en})$ where $H^{\prime}_{ei}=f(H_{ei})$ for all $H_{ei}\in[H_{e}]$ , whereby the function $f$ is defined to satisfy the following propertiy:

$f(x)\subseteq f(y)$ , iff and only iff for any increasing sequences $x,y\in[H_{e}],x\subseteq y$ .

This means that [ $H^{\prime}_{e}$ ] is in itself an increasing sequences if $f$ is monotonic. Apparently composition of two monotonic functions $f$ and $g$ is monotonic, i.e., their composition satisfies:

$\displaystyle f\circ g(x)\subseteq f\circ g(y)\ \textit{iff}\ x\subseteq y$ (16)

There exists a unique minimal solution to the fixed point equation, with a monotonic function over a complete partial order:

$\displaystyle x=f(y)$ (17)

When a function is a monotone mapping over a complete partial order, there exists a unique minimum fixed point corresponding to the history of interaction among processes (services). Since the least fixed point is unique, these histories are determined by the definitions of the elementary services, the relations representing the correspondence of events, and the number of interaction. This means the result of interaction is determined by the definition of the composition and is not influenced by the choice of execution order of processes, i.e. an IWSN instance is determinate.

Theorem 2 (Compatible). In an execution $e$ of an IWSN, if effective( $e$ ), then compatible( $p, q$ ), for some $p,q\in_{S}$ , $S$ is the set of Services in this network.

Proof. To proving that iff for $\forall p$ , $q\in P$ , $p$ and $q$ are two interactive web services, then compatible( $p, q$ ) establish. Let execution( $e_{1}$ ) $=o_{1}o_{2}\ldots o_{i}$ , execution( $e_{2}$ ) $=b_{1}b_{2}\ldots b_{i}$ . In terms of behavior compatibility of Definition 4, we need to consider write/read operations in the communication channels between this two services. For a communication channel, write operation precedes its corresponding read operation. According to Definition 5, if $a_{1}$ is a writing action in execution( $e_{1}$ ), there must exist $b_{1}$ is the corresponding read action in execution( $e_{2}$ ). Since a channel is of FIFO queue structure, the message $a_{1}$ in channel c must be read first in execution( $e_{2}$ ). So, $b_{i}$ has to be the first operation in execution( $e_{2}$ ), that is, $b_{i}=b_{1}$ . For the same reason, $b_{2}$ is the opposite operation of $a_{2}$ , and so on, in the end, the behavior trace for $e_{1}$ , $e_{2}$ is exactly opposite. This satisfies the behavior compatibility in Definition 4, i.e. compatible( $p$ , $q$ ) is satisfied.
7. Case study

7.1 A consulting service for the care burden of diabetic patients’ caregivers

To verify the feasibility of using our method to implement the function of health supplemented software, we will demonstrate the application of IWSN through a healthcare-related service in a simple scenario, i.e., a Consulting Service for the Care Burden of Elderly Diabetic Patients’ Caregivers, which is designed to provide the information about the care burden of elderly diabetic patients’ caregivers that can be the the scientific basis for the competent department to formulate policies aiming at reducing the care burden of caregivers. As illustated in Fig. 4., there are three services involved in this scenario: Care Burden Consulting Service (Consulting Service in short), Caregiver information database service (Database Service in short), and Data Analyzing Service (Analyzing Service in short). As a bridge between users and the Analyzing Service, the Consulting Service could process the received data and interact with users in the form of voice.

Table 3
Messages and their meanings

Messages	Explicit meanings
Info_Consult:	Message sent from users to the Consulting Service. Users expect to obtain information about the care burden of the diabetic patients’ caregivers and request the Consulting Service to provide.
Req_Data_Analyze	Message sent from the Consulting Service to the Analyzing Service. The Consulting Service expect to obtain the analysis result of the care burden data of the diabetic patients’ caregivers and request the Analyzing Service to provide.
Req_Data	Message sent from the Analyzing Service to the Database Service. The Analyzing Service needs the the care burden data of the diabetic patients’ caregivers and request the Database Service to provide.
Data_Sen	Message sent from the Database Service to the Analyzing Service. The Database Service transmit the related data requested by the Analyzing service to it.
Analysis_resul	Message sent from the Analyzing Service to the Consulting Service. The Analyzing Service transmit the analysis results of care burden data of diabetic caregivers expected by the Consulting Services to it.
Info_Reply	Message sent from the Consulting Service to users. The Consulting Service processes the data received from the Analyzing Service and provide users with the information about the care burden of the diabetic patients’ caregivers expected by them.

Figure 4.

A consulting service for the care burden of elderly diabetic patients’ caregivers.

The workflow of this composite service is introduced briefly as follows: When there is a need to know the caregiver’s care burden, the competent department requests to invoke the Consulting Service. The Consulting Service, after receiving the invoke request, request to invoke the Analyzing Service to obtain the analysis results of data related to caregivers. When receiving the invoke request from the Consulting Service, Analyzing Service request to invoke Database Service to obtain the related data, analyze the received data and transmit the analysis results back to the Consulting Service. Consulting Service will then provide the competent department with the expected information.

The messages of Pi-calculus are used to formalize the interactive operations performed by services. Meaning of the messages is shown in Table 3.

By means of the Behavior Semantics of IWSN defined in Section 6, the corresponding Pi-calculus expressions can be obtained as follows:

Consulting _Service $=$ Info_Consult. !Req_Data_Analyze. Analysis_result. Info_Reply Analyzing_Service $=$ Req_Data_Analyze. !Req_Data. Data_Send. !Analysis_result Database_Service $=$ Req_Data. !Data_Send Composite_Service $=$ ( Consulting_Service $|$ DB_Analysis_Service $|$ DB_Service ) / { Req_Data_ Analyze, Analysis_result, Data_Send}

The relation Behavior Compatibility given in Definition 4 is a relation between the evolutions of two processes such that for each evolution of one of the processes there exists a corresponding evolution of the another process, such that their evolutions are observationally equivalent and lead to processes which are again compatible. Using the definition of Behavior Compatibility could helps service designers optimize their composite services by, e.g., changing the component web services with compatible ones.

In our scenario users interact with the composite services Composite_Service. If the behavior of user and Composite_Service are described respectively as: Users $=$ !Info_Consult. Info_Reply, Composite_Service $=$ Consulting_Service $|$ DB_Analysis_Service $|$ DB_Service. According to Definition 4 we need the opposite behavior trace of user: Users $=$ Info_Consult. Info_Reply. Then by executing the command CWB-NC, we will examine whether this two processes are compatible.

7.2 Verification of the services interactive behavior

The process of design and validation of a service composition can be assisted by formal description and verification tool. The application of Pi-calculus in the design phase of the composition helps designers showexplicitly the interaction of the services that make up the system. After the system model has been constructed, modal $\mu$ -calculus [19] can be utilized to infer the behavior of the system.

Reachability analysis is the first procedure in the process of system verification, which needs to compose a logical formula specifying a “undesired state” that the system should not reach in $\mu$ -calculus. The specification will be processed by CWB-NC and checked for syntactic correctness first. CWB-NC will next exploit every possible state the system may present during runtime and checks to confirm whether an undesired state is reachable. When an undesired state is sensed, a description that record the historic execution sequence leading to that state will be displayed. Defects in the system design Such as deadlock and fatal section violation may be detected in this process. One of the elementary properties system must satisfy is the correct termination. We use string Could_Terminate to indicate the termination state of a system, of which the detailed explanation is: Could_Terminate is true if this system will reach a terminative state. This property the system should reach expressed in $\mu$ -calculus is as following:

$\displaystyle\textit{prop Could{\_}Terminate}=\textit{min}X=[-]\textit{ff}\ % \vee<->X$ (18)

The definition of Behavior Compatibility helps designer optimize service composition by, for instance, changing an component services with a compatible one. Another merit is the customization of services. In order to upgrade service quality, service providers may adjust their services for the convenience of customers, and the behavior of this custom service should be compatible with the original service. The relation Behavior Compatibility we defined in Definition 4 is actually a relation indicating for two processes there exist some evolutions from them and for every evolution of one of them there exist a corresponding evolution of the another such that these two evolutions are observationally equivalent, which will lead to processes compatible again. To carry out compatible verification, we need to express both systems and specifications in Pi-calculus, whereby the specification describe the behavior of a system much more abstractly than the system description. In the scenario presented above users interacts with the services composition Composite_Service. According to Definition 4, the opposite behavi or trace of users and the behavior of Composite_Service are as follows:

!Users $=$ Info_Consult. ? Info_Reply; Composite_Service $=$ Consulting_Service $|$ DB_Analysis_Service $|$ DB_Service.

At this moment, by typing the command ‘eq -S obseq’ into CWB-NC tool, whether this two processes are compatible can be examined.

7.3 Data analysis results

The test site of the above experiment was located in the Endocrinology Department of a top hospital in Inner Mongolia Autonomous Region and relevant data analysis results was obtained. The data sets of this experiment comes from the on-line survey of 158 in-patient elderly diabetics and their main caregivers in the Endocrinology Department from January 2018 to June 2018 based on convenience sampling method.

7.3.1 Status quo of the care burden of elderly diabetic patients’ caregivers

The care burden scale is Zarit Burden Interview (ZBI) [20], of which the Cronbach’s $\alpha$ coefficient was 0.88 and the retest reliability was 0.87. The scores was 37.33 $\pm$ 16.33 in reference to the care burden of the 158 caregivers, meaning the care burden level for them is mild. See the Tables 4 and 5 for detailed results of care burden.

Table 4
Score of care burden scale of the main caregivers for the elderly diabetic patients ( $n=$ 158)

Current situation of care burden of main caregivers	Maximum value	Mean value	Standard deviation
Personal Burden	48	21.74	8.91
Responsibility Burden	24	10.09	5.42
Score of the scale	88	37.33	16.33

Table 5

Incidence of care burden in the main caregivers ( $n=$ 158)

Care burden status	Number of cases	Constituent ratio (%)
Free of Burden	28	17.7
Mild Burden	69	43.7
Moderate Burden	48	30.4
Heavy Burden	13	8.2

7.3.2 Analysis results of multiple factors influencing the care Burden of elderly diabetic patients’ caregivers

There are many factors that influence the care burden of the elderly Diabetic Patients’ Caregivers. Multivariable linear regression was used by the Analyzing Service to further clarify the influence degree of various factors, where the dependent variable was the main caregiver’s care burden score and the independent variables were the statistically significant variables in t-test and single factor test, ADL score and social support scale score.

According to the influencing level of various factors on the care burden, factors included in the regression equation are current situation of self-care, number of hospitalizations due to diabetes, and years of care. Results of multiple regression analysis is shown in the Table 6.

Table 6
Multiple linear regression results of ZBI and independent variable ( $n=$ 158)

Independent variables	Regression coefficient	Standardized regression coefficient	T	$P$
Constant	27.060		6.163	$<$ 0.000
Current Situation of Self-Care	9.433	0.368	5.176	$<$ 0.000
Number of Hospitalizations Due to Diabetes	2.192	0.191	2.690	0.008
Years of Care	$-$ 4.691	$-$ 0.286	$-$ 4.043	$<$ 0.000

Analysis results of variance showed that $F=$ 17.226, $P=$ 0.000, which proved the multivariate linear regression equation was statistically significant and the combination of explanatory variables such as caregiver’s age had a significant effect on the care burden. The goodness of fit test showed that the goodness of fit reaches 0.506 and the variables can explain 24.1% change of the care burden.

8. Conclusions and future works

In this paper, an interaction model of web services based on KPN was proposed, aiming to effectively take the advantage of the flexibility of service composition technology and guarantee the behavior compatibility ofweb services. Formal behavioral semantics of our model was defined by Pi-calculus process algebra. The correctness and completeness of the formal behavior semantics was guaranteed by introducing valuation functions, which were used to translate model descriptions into Pi-calculus expressions. Formal definition of behavior compatibility was given, formal properties of this model was discussed and how the supporting tool, i.e. CWB-NC, could be utilized to verify the properties we anticipate was presented. Finally, our model was demonstrated in a practical case, i.e., a consulting service for the care burden of diabetic patients’ caregivers, of which the experimental results proved that our proposed method is feasible and applicable.

As introduced above, Interactive Web Service Network is based on KPN that has such characteristics as parallelism and communication mechanism, compositional property, executable property, which makes it appropriate to model services interaction. Our future work is to make an effort to implement Interactive Web Service Network for more web service applications in healthcare filed.

Footnotes

Acknowledgments

This work was supported by the National Natural Science Foundation of China under Grant No. 61862048, 61966028.

References

Yang

Zhang

and Ji

, Research on cloud service quality control implementation based on improved load balance algorithm, Journal of Computational Methods in Sciences and Engineering 18(3) (2018), 793–800.

Wang

X.L.

and Dong

G.F.

, Research on cloud computing task scheduling algorithm based on particle swarm optimization, Journal of Computational Methods in Sciences and Engineering 19(2) (2019), 1–9.

Wagner

Ishikawa

and Honiden

, Robust service compositions with functional and location diversity, IEEE Transactions on Services Computing 9(2) (2016), 277–290.

Wang

Ding

and Jiang

, Constrain-aware approach to web service composition, IEEE Transactions on Systems Man & Cybernetics Systems 44(6) (2014), 770–784.

Lemos

A.L.

Daniel

and Benatallah

, Web service composition: A survey of techniques and tools, ACM Comput. Surveys 48(3) (2016), Art. no. 33.

Cleaveland

and Sims

, The Concurrency Workbench of the New Century, Stony Brook Univ., 2000.

Xiong

P.C.

Fan

Y.S.

and Zhou

M.C.

, A petri net approach to analysis and composition of web services, IEEE Transactions on Systems Man and Cybernetics – Part A Systems and Humans 40(2) (2010), 376–387.

Tan

and Zhou

M.C.

, Timed compatibility analysis of web service composition: A modular approach based on petri nets, IEEE ransactions on Automation Science and Engineering 11(2) (2014), 594–606.

Liu

Jiang

and Zhou

, Interactive petri nets, IEEE Transactions on System, Man, and Cybernetics: System 43(2) (2013), 291–302.

10.

Tan

Fan

and Zhou

M.C.

, Data-driven service composition in enterprise SOA solutions: A petri net approach, IEEE Transactions on Automation Science and Engineering 7(3) (2010), 686–694.

11.

El Hadad

Manouvrier

and Rukoz

, TQoS: Transactional and QoS-Aware selection algorithm for automatic web service composition, IEEE Transactions on Services Computing 3(1) (2010), 73–85.

12.

Zhang

Liu

and Abraham

, A novel process network model for interacting context-aware web services, IEEE Transactions on Services Computing 6(3) (2013), 344–357.

13.

Saurabh

Sumit

and Sumit

, Describing and verifying web services composition using Pi-calculus, International Journal of Concurrent Engineering and Scientific Research 3(1) (2016), 2393–8374.

14.

and Lu

, A formal model for BPEL4WS description of web service composition, Wuhan University Journal of Natural Sciences 11(5) (2006), 1311–1319.

15.

Kahn

, The Semantics of a Simple Language for Parallel Programming, Information Processing, North Holland Rosenfeld

J.L.

, ed., 1974, pp. 471-475.

16.

Milner

, Communication and Mobile Systems: The Pi-Calculus, Cambridge University Press, 1999.

17.

Milner

, Communication and Concurrency, Prentice Hall, 1989.

18.

Milner

, A calculi of Communication and Concurrency, Spinger-Verlag, 1980.

19.

Stirling

, Modal logics for communicating systems, Theoretical Computer Science 49(2-3) (1987), 311–347.

20.

Zarit

S.H.

Orr

N.K.

and Zarit

J.M.

, Families under stress: Caring for the patient with Alzheimer’s disease and related disorders, New York: University Press, 1985.

IWSN: A novel method for modeling the interaction of web services

Abstract

Keywords

1. Introduction

4.1 Petri nets based approaches

4.2 Process algebra based approaches

5. Interactive web service network: A service interaction model

5.1 Kahn process network

5.2 Interactive web service network

6.1 Syntax of Pi-calculus

Table 1 The inference rules of Pi-calculus

Table 2 Valuation functions for IWSN

7.1 A consulting service for the care burden of diabetic patients’ caregivers

Table 3 Messages and their meanings

7.3.1 Status quo of the care burden of elderly diabetic patients’ caregivers

Table 4 Score of care burden scale of the main caregivers for the elderly diabetic patients ( n = 158)

Table 6 Multiple linear regression results of ZBI and independent variable ( n = 158)

Footnotes

Acknowledgments

References

Table 1
The inference rules of Pi-calculus

Table 2
Valuation functions for IWSN

Table 3
Messages and their meanings

Table 4
Score of care burden scale of the main caregivers for the elderly diabetic patients ( $n=$ 158)

Table 6
Multiple linear regression results of ZBI and independent variable ( $n=$ 158)