本技术公开了一种云网融合环境下基于概率模型检验的服务组合验证方法及系统。本发明通过收集云网用户位置信息、服务器分布和服务质量文件,通过融合云网用户位置信息、服务器分布和服务质量文件得到云网服务样本数据集。在此基础上,对云网融合中的服务组合过程进行形式化建模,同时考虑了用户移动导致的云网融合环境下服务属性的变化。将用户位置信息作为历史数据,利用马尔可夫过程建立了用户移动模型。为了准确描述用户需求,对云网融合场景下的用户需求进行多目标形式化描述,利用PRISM模型检验工具来进行云网融合环境下的服务组合验证。本发明提出的服务组合验证方法能够及时验证服务组合是否满足用户需求,以确保服务组合仍然满足性能和可用性要求。
背景技术
随着面向服务体系结构的不断成熟,服务组合成为了一个关键概念。服务组合是将单一的服务组合成一个新的服务,以满足特定需求的过程。近年来,服务组合不仅在传统环境下得到应用,也在云网融合环境中发挥关键作用。在云网融合环境下,服务之间的相互作用和依赖关系变得更加复杂,因此,服务组合验证变得尤为重要。基于模型检验的验证技术能够发现服务组合过程中的问题,并评估服务组合的性能指标,从而协助质量控制过程,减少由于服务组合错误而带来的损失。
近年来,已经有大量研究致力于服务组合验证问题,对服务组合进行建模,根据CTL,PCTL等形式化语言对用户需求进行描述,将服务组合模型和用户需求输入到模型检查器中进行验证,这些方法在传统环境下的服务组合验证中取得了一些进展。Bataineh等人提出了一种基于代理的服务组合方法的模型检查方法。在这种方法中,创建一个BPEL模型来转换为一个自动机模型,虽然该方法考虑了服务组合中各个服务的依赖关系,但该方法只对服务组合的正确性进行了验证,对于其他属性验证的可行性仍需进一步考虑。Mietal等人提出了一种基于概率的模型检查,以使用Markova模型组合Web子服务,首先,使用BPEL语言在组合方法中向每个子服务添加可靠性属性,然后,使用Markova决策流程描述服务选择过程。最后,在PRISM模型检查器中分析CTL公式。虽然该方法特别考虑了可靠性属性,但容易导致状态爆炸问题,不适用于服务数量大的服务组合验证。
当前云网融合环境下服务的验证方法存在问题,在云网融合环境下,用户呈现出移动性特征,这导致用户可能在短时间内从一个服务场景转移到另一个服务场景,这使得在验证过程中上一个服务的选择概率和属性值失效,直接增加了验证难度。同时,云网融合环境下服务呈现出规模庞大的特点,因此,需要在服务组合验证过程中考虑到用户的移动性和服务数量庞大的问题,对服务组合进行验证。
实现思路