摘要：

随着云网融合技术以及空天地一体化网络的快速发展, 越来越多的服务开始在云网融合环境下运行。在云网融合环境下, 用户呈现移动性特征, 导致服务组合过程变得愈发复杂, 服务组合验证变得尤为关键。同时, 在云网融合环境下用户要求服务组合不仅在当前时间段内稳定运行, 还需要在未来时间段内持续满足用户需求。为了解决以上问题, 提出一种云网融合环境下的服务组合未来属性验证方法。首先, 对云网融合中的服务组合过程进行形式化建模, 同时考虑用户移动导致的云网环境下服务场景的转换关系; 然后, 为了准确描述用户需求, 对云网融合场景下的用户需求进行形式化描述; 最后, 为了解决云网融合环境下用户对服务组合未来时间段内的验证需求, 对服务组合未来时间段的服务属性进行预测, 利用PRISM模型检验工具来进行云网融合环境下的服务组合验证, 以确保在未来时间段内仍然满足性能和可用性要求。实验结果表明, 在云网融合环境下, 当服务数量达到1 000时验证模型构建时间以及模型检测时间分别为3.372 s和0.075 s, 通过云网融合环境下的服务组合案例说明了所提方法的有效性与可行性。

关键词: 云网融合, 服务组合, 马尔可夫决策过程, 服务质量, 形式化验证

Abstract:

With the rapid development of cloud network integration technology and integration of air and space networks, an increasing number of services are transitioning to operate within this integrated environment. In the context of cloud-network integration, users exhibit mobility characteristics, leading to heightened complexity in service composition. Consequently, the validation of the service composition is critical in the context of cloud network integration. Simultaneously, the cloud-network integration paradigm demands that service compositions not only function reliably in the present timeframe but also sustainably cater to future demands. This paper proposes a method for verifying the future attributes of service compositions in a cloud-network integration environment. Initially, the method formalizes the service composition process within the context of cloud network integration by considering the transformation relationships among the service scenarios in this environment. Subsequently, formal descriptions of user needs in cloud-network integration scenarios are provided to accurately describe user needs. Finally, to address the verification needs for future timeframes, the attributes of service compositions for upcoming periods are predicted using the PRISM validation tool. The experimental results showed that the validation model construction time and model inspection time were 3.372 s and 0.075 s, respectively, when the number of services reached 1 000 in the cloud-network fusion environment. The effectiveness and feasibility of this method were demonstrated through service composition cases in a cloud network fusion environment.

Key words: cloud-network integration, service composition, Markov Decision Process(MDP), Quality of Service(QoS), formal verification