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.
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.
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.
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.
State transition graph of the participating services.
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
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
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
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].
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.
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.
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.
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.
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.
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.
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
Service is a set of web services;
Process denotes a set of processes;
Operation denotes a set of operations;
Message denotes a set of messages transmitted to and from processes;
We let
where:
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.
Syntax of Pi-calculus
In Pi-calculus processes are denoted by capital letters
A null process written as 0, meaning this process terminates; symbol
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:
The inference rules of Pi-calculus
The inference rules of Pi-calculus
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,
Valuation functions for IWSN
Valuation functions for IWSN
Valuation functions are defined as follows:
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:
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.
Let
whenever
If there is a weak bisimulation relation
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
Obviously, the relation
Since for every increasing sequence, there exists a least upper bound that is also in set [
This means that [
There exists a unique minimal solution to the fixed point equation, with a monotonic function over a complete partial order:
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.
Proof. To proving that iff for
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.
Messages and their meanings
Messages and their meanings
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
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
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
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
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
At this moment, by typing the command ‘eq -S obseq’ into CWB-NC tool, whether this two processes are compatible can be examined.
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.
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
Score of care burden scale of the main caregivers for the elderly diabetic patients (
158)
Score of care burden scale of the main caregivers for the elderly diabetic patients (
Incidence of care burden in the main 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.
Multiple linear regression results of ZBI and independent variable (
158)
Multiple linear regression results of ZBI and independent variable (
Analysis results of variance showed that
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.
