Journal of Computer Applications ›› 2020, Vol. 40 ›› Issue (11): 3267-3272.DOI: 10.11772/j.issn.1001-9081.2020030387

• Computer software technology • Previous Articles     Next Articles

QoS verification of microservice composition platform based on model checking

MAO Xinyi, NIU Jun, DING Xueer, ZHANG Kaile   

  1. Faculty of Electrical Engineering and Computer Science, Ningbo University, Ningbo Zhejiang 315211, China
  • Received:2020-03-31 Revised:2020-05-14 Online:2020-11-10 Published:2020-06-18
  • Supported by:
    This work is partially supported by the Open Subject of Key Laboratory of Embedded System and Service Computing of Ministry of Education (ESSCKF201907), the Ningbo Natural Science Foundation (2019A610088).

基于模型检测的微服务组合平台QoS验证

毛昕怡, 钮俊, 丁雪儿, 张开乐   

  1. 宁波大学 信息科学与工程学院, 浙江 宁波 315211
  • 通讯作者: 钮俊(1976-),男,四川阆中人,副教授,博士,CCF会员,主要研究方向:服务计算、模型检测、物联网;niujun@nbu.edu.cn
  • 作者简介:毛昕怡(1993-),女,浙江衢州人,硕士研究生,主要研究方向:服务计算、模型检测;丁雪儿(1996-),女,浙江宁波人,硕士研究生,主要研究方向:代码搜索、代码推荐;张开乐(1994-),男,浙江宁波人,硕士研究生,主要研究方向:代码搜索、机器学习
  • 基金资助:
    教育部嵌入式系统与服务计算重点实验室开放课题(ESSCKF2019-07);宁波市自然科学基金资助项目(2019A610088)。

Abstract: Concerning the problem that microservice composition platform is short of analysis and verification of Quality of Service (QoS) indicators, a formal verification method based on model checking was proposed to analyze and evaluate the factors that affect the microservice composite platform performance. First, the service resource configuration process of microservice composition was divided into three phases:service request, configuration and service execution. These three phases were implemented by three modules:service request queue, resource configurator of service requests and virtual machine for providing service resources. After that, the implementation processes of the three modules were modeled as Labelled Markov Reward Models (LMRM), and the global model of microservice composition process was obtained by using a synchronization concept similar to the process algebra. Then, the logic formula of continuous random reward logic was used to describe the expected QoS indicators. Last, the formal model and logic formula were regarded as the input of model detection tool PRISM to obtain the verification results. Experimental results prove that LMRM can realize the QoS verification and analysis as well as the construction of microservice composite platform.

Key words: microservice composition, continuous-time Markov chain, continuous stochastic reward logic, model checking, PRISM

摘要: 针对当前缺少对微服务组合平台的服务质量(QoS)指标进行分析验证的问题,提出一种基于模型检测的形式化验证方法,对影响微服务平台性能的因素进行分析评估。首先,将微服务组合的服务资源配置过程划分为服务请求、资源配置和服务执行3个阶段,并分别由服务请求队列、服务请求配置器和提供服务资源的虚拟机等模块实现;其次,将各个模块的实现过程建模为带标记Markov回报模型(LMRM),借助类似于进程代数的同步概念获得微服务组合过程的全局模型;接着,用连续随机回报逻辑公式刻画期望的QoS指标;最后,将形式模型与逻辑公式作为模型检测工具PRISM的输入以获得验证结果。实验结果表明,LMRM可较好地用于微服务组合平台的建模和QoS验证分析。

关键词: 微服务组合, 连续时间Markov链, 连续随机回报逻辑, 模型检测, PRISM

CLC Number: