聚合型时序逻辑驱动的复合服务联动定量监测  

Compositional Temporal Logic for Associative Quantitative Monitoring of Composite Services

作　　者：周长兵[1,2] 赵登 张文博[3] 孙骁 薛霄[5] ZHOU Zhang-Bing;ZHAO Deng;ZHANG Wen-Bo;SUN Xiao;XUE Xiao(School of Information Engineering,China University of Geosciences,Beijing 100083,China;Frontiers Science Center for Deep-time Digital Earth,China University of Geosciences,Beijing 100083,China;Institute of Software,Chinese Academy of Sciences,Beijing 100190,China;Department of Automation,Tsinghua University,Beijing 100084,China;College of Intelligence and Computing,Tianjin University,Tianjin 300072,China)

机构地区：[1]中国地质大学(北京)信息工程学院,北京100083 [2]中国地质大学(北京)深时数字地球前沿科学中心,北京100083 [3]中国科学院软件研究所,北京100190 [4]清华大学自动化系,北京100084 [5]天津大学智能与计算学部,天津300072

出　　处：《软件学报》2024年第12期5419-5451,共33页Journal of Software

基　　金：中央高校基本科研业务费(2652023001);国家自然科学基金(62372420,42050103);地质调查专项“地球科学文献知识服务与决策支撑二级项目”(DD20230139)。

摘　　要：近年来,面向服务的物联网体系架构受到学术界和工业界的广泛关注.通过把物联网资源虚拟化为智能物联网服务,动态互联并融合协同这些资源受限且动态演进的物联网服务,从而构建物联网应用,已成为一种被普遍认可且灵活有效的机制.面向边缘设备资源稀缺且动态时变,物联网服务在其执行过程中可能发生QoS变化或资源失配,致使物联网应用难以继续或可能诱使故障发生.因此,实现物联网服务的实时定量监测,已成为保障物联网应用鲁棒性和系统健壮性的关键.现有相关研究工作提出了不同监测机制,但其在形式化解释上仍存不足,表现为较强的领域相关性和经验主观性.基于形式化方法,例如信号时序逻辑,可将物联网服务运行态实时定量监测问题转换为时序逻辑任务.然而,现有信号时序逻辑存在信号不可辨性、方法不鲁棒性以及场景不适用性问题.并且,在物联网服务以复合服务形式监测时,现有工作存在整体性、联动性、动态性考虑不足的问题.为解决上述问题,提出一种聚合型信号时序逻辑,以实现单个服务、服务之间以及复合服务上不同QoS约束和时间约束的实时联动定量监测.所提方法扩展基于正负偏置黎曼和的累加型时间算子,对整个时间域内所有子公式进行鲁棒性度量,实现时序鲁棒、信号可辨、动态适用的物联网服务运行态实时定量监测;并扩展基于约束类型与组合结构的聚合算子,以及随动态环境可变的动态变量,实现复合服务在动态环境中的联动定量监测.由此,物联网服务及其复合服务的多维度多约束被转换为逻辑公式,并在运行时以定性和定量化的满意度进行形式化解释.实验结果表明所提方法具有更好的监测表达能力、场景适用性和结果鲁棒性.In recent years,service-oriented IoT architectures have received a lot of attention from academia and industry.By encapsulating IoT resources into intelligent IoT services,interconnecting and collaborating these resource-constrained and capacity-evolving IoT services to facilitate IoT applications has become a widely adopted and flexible mechanism.Upon capacity-fluctuating and resource-varying edge devices,IoT services may experience QoS degradations or resource mismatches during their execution,making it difficult for IoT applications to continue and possibly inducing failures.Therefore,quantitative monitoring of IoT services at runtime has become the key to guaranteeing the robustness of IoT applications.Different monitoring mechanisms have been proposed in recent literature,but they are inadequate in formal interpretation with strong domain relevance and empirical subjectivity.Based on formal methods,such as signal temporal logic(STL),the problem of IoT service monitoring can be formulated as a temporal logic task to achieve runtime quantitative monitoring.However,STL and its extensions suffer from issues of non-differentiability,loss of soundness,and inapplicability in dynamic environments.Moreover,existing works are inadequate for the monitoring of composite services,with a lack of integrity,linkage,and dynamics.To solve these problems,this study proposes a compositional signal temporal logic(CSTL)to achieve quantitative monitoring of different QoS constraints and time constraints upon intra-,inter-,and composite services.Specifically,CSTL extends an accumulative operator based on positively and negatively biased Riemann sums to emphasize the robust satisfaction of all sub-formulae over their entire time domains and to evaluate qualitative and quantitative constraint satisfaction for IoT service monitoring.Besides,CSTL extends a compositional operator based on constraint types and composite structures,as well as dynamic variables that can vary with the dynamic environment,to effectively monitor QoS variation

关 键 词：物联网服务 复合服务 定量监测 实时监测 信号时序逻辑 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]