聚合型时序逻辑驱动的复合服务联动定量监测
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

TP311

基金项目:

中央高校基本科研业务费深时数字地球前沿科学中心“深时数字地球”中央高校科技领军人才团队项目(2652023001); 国家自然科学基金(62372420, 42050103); 地质调查专项“地球科学文献知识服务与决策支撑二级项目”(DD20230139)


Compositional Signal Temporal Logic for Runtime Quantitative Monitoring of Composite Services
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    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 variations and temporal violations of composite services. As a result, temporal and QoS constraints upon intra-, inter-, and composite services, can be specified by CSTL formulae, and formally interpreted with qualitative and quantitative satisfaction at runtime. Extensive evaluations show that the proposed CSTL performs better than baseline techniques in terms of expressiveness, applicability, and robustness.

    参考文献
    相似文献
    引证文献
引用本文

周长兵,赵登,张文博,孙骁,薛霄.聚合型时序逻辑驱动的复合服务联动定量监测.软件学报,,():1-33

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2023-05-08
  • 最后修改日期:2023-07-21
  • 录用日期:
  • 在线发布日期: 2024-03-13
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号