Service oriented software systems running in a highly open, dynamic and unpredictable Internet environment are inevitable to face all kinds of uncertainty. To monitor the operation of the web services system behavior analysis and analysis whether the system behavior is consistent with the requirements is the basis to determine whether the system needs to be reconfigured. In this paper, an analytical platform for the behavior of a web service-oriented system based on the probabilistic model checking is introduced which provides the basis for judging whether a system needs to be reconfigured by applying the approach of probabilistic model checking to verify whether the behavior system model is satisfied requirement properties. This platform is implemented in Java language and using the dot tool that the Graphviz provides and the PRISM model checker to construct the behavior model of the web service-oriented system based on web log files, to view and edit behavior models visually, and to convert the model from one form to another to make it convenience for users to use the model checker PRISM. Finally, we can judge whether the model is satisfied the desired requirements according to the verification result.
Top1. Introduction
SOA (service-oriented Architecture, Service - Oriented Architecture) provides a loosely coupled distributed computing paradigm. On the basis of technology standardization system consisting of WSDL, UDDI, SOAP etc., different types and forms of the upper business functions and data and computing resources is described and published and discovered and accessed in a unified way, thus, a computing environment surrounding of Service (WS, Web Service) is formed based on the standard and open internet technology.
Web services can be directly integrated application system based on Service or composed in some business process description language to realize the more complex business functions. The composed business process still can be accessed in the manner of web service. SBA and SBS are all called the web service–oriented system.
Web service system operating in a highly open, dynamic and unpredictable Internet environment, therefore, is inevitable to face all kinds of uncertainty, for example, the uncertainty of the number of accessing users, page views, the duration of the visit page, and the uncertainty of the user types, the process that user use, and the uncertain value that by uncertain access processes, etc.
The traditional software system adopts the design approach based on premised, in this way, the software system is not flexible, software runs unstable and unreliable, unable to respond to the use of all kinds of uncertain environment Adaptive configuration software needs, therefore, to ensure that the core business process of survivability, reliability and availability, such as nature, to ensure that the service provider market competitiveness
Self-adaptive systems mean that software has autonomous capabilities, which can also be explained with reference to autonomic computing’s use of a monitor-analyze-plan-execute, or MAPE, closed control loop to achieve self-management in computer systems. The four stages of the MAPE loop are enabled by knowledge.
From the MAPE feedback control loop structure, we can find that it is the primary task to monitor and analysis the behavior of web service oriented systems. So, we design and implement an analytical platform for the behavior of a web service-oriented system based on the probabilistic model checking to provide the basis for judge whether a system needs to be reconfigured by adopting the approach of probabilistic model checking to verify whether the behavior system model is satisfied requirement properties.
The remainder of the paper is structured as follows. Section 2 introduces some basic concepts and the tools about PRISM and Graphviz which we have integrated into our platform. Section 3 presents the approach of constructing the running behavior model for a web service system based on web log files and secondly, presents to extend the running behavior model with business value to express the potential domain knowledge, and finally presents to product the requirement property formula based on the extended model. Section 4 describes the architecture of the platform and the functionalities of the subservices which consist of the platform in detail. In this section, the algorithm of each subservice is discussed and the snapshot of it is also presented. Section 5 concludes the paper and lists planned further work.