Automated Quantitative Verification for Service-Based System Design: A Visualization Transform Tool Perspective
Automated Quantitative Verification for Service-Based System Design: A Visualization Transform Tool Perspective
复制标题
DOI：
10.1142/s0218194018500390
复制
发表时间：
2018-09
期刊：
影响因子：
--
通讯作者：
Honghao Gao;Huai-kou Miao;Lilan Liu;Jinyu Kai;Kun Zhao
中科院分区：
文献类型：
--
作者：
Honghao Gao;Huai-kou Miao;Lilan Liu;Jinyu Kai;Kun Zhao
基于服务的系统是一种新的分布式业务过程集成的软件模式。传统的测试方法很难验证软件的功能需求和非功能需求。为了解决这个问题，本文提出了一个可视化的验证平台，定量计算的可靠性和成本评估基于服务的系统在设计阶段的性能。首先，提出了一个扩展的自动机模型，即概率奖励标记转换系统（PRLTS）的功能性行为和非功能性功能的形式化。然后介绍了概率模型检测器PRISM的形式化语言，给出了要转换的目标验证码的文法。其次，对业务流程执行语言XML描述标记进行解析，利用不同的转换规则生成功能行为，并在此基础上采用概率矩阵和报酬概念分别表示服务的可靠性和成本。第三，将PRLTS模型转化为PRISM的输入语言，以Graphviz的图形描述语言DOT为中介，以可视化的方式显示系统行为。模型布局允许设计者手动调整PRLTS模型的行为，其中验证码可以根据修改信息的变化动态更新。第四，为了进行定量验证，可以在输入基于服务的系统的需求模型时自动生成概率计算树逻辑（ProbabilityComputationTreeLogic，PCTL）公式形式的验证属性，在此过程中，初始计算定性属性的阈值并将其作为推荐值返回。这允许用户以交互方式修改定性属性。最后，通过对实际案例的实验分析，验证了该方法的可行性。因此，我们的平台为定量验证和图形可视化提供了指导，以有效地生成正式模型并检查基于服务的系统的定量属性。
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.