Automated Quantitative Verification for Service-Based System Design: A Visualization Transform Tool Perspective

作者：Gao, Honghao; Miao, Huaikou^*; Liu, Lilan; Kai, Jinyu; Zhao, Kun

来源：International Journal of Software Engineering and Knowledge Engineering, 2018, 28(10): 1369-1397.

DOI：10.1142/S0218194018500390

• Service system
• design visualization
• quantitative verification
• probabilistic model checking
• model transformations

Service-based systems are a new software mode for distributed business processes integration. It is difficult for traditional testing methods to verify the functional and nonfunctional requirements of software. To address this problem, this paper proposes a visual verification platform to quantitatively compute the reliability and cost for evaluating the performance of service-based systems in the design phase. First, an extended automata model namely Probabilistic Reward Labeled Transition System (PRLTS) is proposed to formalize both the functional behaviors and nonfunctional features. Then, the formal language of probabilistic model checker PRISM is introduced to show the grammar of the target verification codes that we want to transform. Second, XML description tags of Business Process Execution Language (BPEL) is parsed to generate the functional behaviors using different kinds of transformation rules, based on which the probability matrix and reward concept are employed to denote the service's reliability and cost, respectively. Third, the PRLTS model is turned into the input language of PRISM, where the graphic description language DOT of Graphviz is used as an intermediary to display system behaviors in a visual way. The model layout allows the designer to manually adjust the behaviors of the PRLTS model, where verification codes can be dynamically updated according to the changes in modified information. Fourth, to perform quantitative verification, the verification property in the form of the Probabilistic Computation Tree Logic (PCTL) formula can be automatically generated when the requirement model of the service-based system is inputted, during which the threshold value of qualitative property will be initially computed and returned as a recommended value. This allows the user to modify the qualitative property in an interactive way. Furthermore, experimental analysis of the real-world case study demonstrates the feasibility of the proposed method. Thus, our platform provides guidance for quantitative verification and graphical visualization for effectively generating formal models and checking the quantitative properties for service-based systems.

• 出版日期2018-10
• 单位上海大学