计算机应用

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

单位：宁波大学 信息科学与工程学院, 浙江 宁波 315211

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

基金：教育部嵌入式系统与服务计算重点实验室开放课题（ESSCKF2019-07）；宁波市自然科学基金资助项目（2019A610088）。

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

来源：2020年第11期

《计算机应用》期刊编辑部

查看计算机应用杂志2020年第11期