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