软件学报

作者：周长兵，赵登，张文博，孙骁，薛霄

单位：周长兵，中国地质大学(北京) 信息工程学院, 北京 100083;中国地质大学(北京) 深时数字地球前沿科学中心, 北京 10008311,赵登，中国地质大学(北京) 信息工程学院, 北京 100083;中国地质大学(北京) 深时数字地球前沿科学中心, 北京 10008302,张文博，中国科学院 软件研究所, 北京 10019003,孙骁，清华大学 自动化系, 北京 10008404,薛霄，天津大学 智能与计算学部, 天津 30007205

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

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

近年来, 面向服务的物联网体系架构受到学术界和工业界的广泛关注. 通过把物联网资源虚拟化为智能物联网服务, 动态互联并融合协同这些资源受限且动态演进的物联网服务, 从而构建物联网应用, 已成为一种被普遍认可且灵活有效的机制. 面向边缘设备资源稀缺且动态时变, 物联网服务在其执行过程中可能发生QoS变化或资源失配, 致使物联网应用难以继续或可能诱使故障发生. 因此, 实现物联网服务的实时定量监测, 已成为保障物联网应用鲁棒性和系统健壮性的关键. 现有相关研究工作提出了不同监测机制, 但其在形式化解释上仍存不足, 表现为较强的领域相关性和经验主观性. 基于形式化方法, 例如信号时序逻辑, 可将物联网服务运行态实时定量监测问题转换为时序逻辑任务. 然而, 现有信号时序逻辑存在信号不可辨性、方法不鲁棒性以及场景不适用性问题. 并且, 在物联网服务以复合服务形式监测时, 现有工作存在整体性、联动性、动态性考虑不足的问题. 为解决上述问题, 提出一种聚合型信号时序逻辑, 以实现单个服务、服务之间以及复合服务上不同QoS约束和时间约束的实时联动定量监测. 所提方法扩展基于正负偏置黎曼和的累加型时间算子, 对整个时间域内所有子公式进行鲁棒性度量, 实现时序鲁棒、信号可辨、动态适用的物联网服务运行态实时定量监测; 并扩展基于约束类型与组合结构的聚合算子, 以及随动态环境可变的动态变量, 实现复合服务在动态环境中的联动定量监测. 由此, 物联网服务及其复合服务的多维度多约束被转换为逻辑公式, 并在运行时以定性和定量化的满意度进行形式化解释. 实验结果表明所提方法具有更好的监测表达能力、场景适用性和结果鲁棒性.

来源：2024年第12期

《软件学报》期刊编辑部

查看软件学报杂志2024年第12期