赵登/周长兵：基于累加型信号时序逻辑的物联网服务实时定量监测机制【IEEE TMC, 2023】

2023-09-13     发布：[bat365正版唯一官网]    点击：250次

考虑到物联网服务在其执行期间，其QoS约束满足程度可能发生动态变化，对物联网服务进行实时定量监测已成为保证物联网服务组合方案鲁棒性的关键。目前已有相关研究工作提出了各种不同服务监测机制，例如采用诸如适应度之类的数学函数，来合理地定量计算物联网服务实时约束满足度。但这些监测工作在形式化解释上仍存不足，表现为较强的领域相关性和作者主观性。基于形式化方法，例如信号时序逻辑，不仅可规约定性化的约束，还可对约束满足度进行定量分析。但是，传统的信号时序逻辑存在信号值迥异、满足度可能无差异的不可分辨性问题。现有研究工作已注意到该缺陷，从均值算子、平滑算子入手，对信号时序逻辑进行增强。然而，这些工作存在不满足约束的信号值被满足约束的信号值所覆盖导致的不鲁棒性问题。针对信号值不鲁棒性缺陷，近期研究工作对满足约束的信号值和不满足部分分别定义其定量化语义。需要强调的是，这些工作基于固定采样率的假定，难以适用于动态变动时信号采样速率难以固定的问题。

针对上述科学问题，我校bat365正版唯一官网赵登老师和周长兵教授、美国佐治亚州立大学蔡志鹏老师、法国图卢兹大学Sami Yangui老师，以及天津大学薛霄教授，对信号时序逻辑拓展时间算子，构建一种累加型信号时序逻辑，实现时序鲁棒、信号可辨、动态适用的物联网服务运行态定量监测。该工作的主要贡献如下：

（1）首先，将物联网服务实时定量监测问题规约为资源动态变化的物联网网络中约束满足问题，并考虑到物联网服务多维QoS约束的动态变化，包括时间约束、空间临近度、能量有限性和资源限制性（图1）。

（2）其次，基于传统信号时序逻辑扩展一种基于正负偏置黎曼和的累加型时间算子，实现整个时间域内所有子公式的鲁棒性度量，即构建一种累加型信号时序逻辑（Accumulative Signal Temporal Logic，记作ASTL），以解决现有研究工作中存在的信号不可辨、鲁棒性不足、动态环境不适用等问题。

（3）然后，基于所构建的累加型信号时序逻辑实现时序鲁棒、信号可辨、动态适用的物联网服务运行态实时定量监测机制，其中物联网服务的多维度多约束被转换为ASTL公式，并在运行时以定性化和定量化的满意度进行形式化解释。并为了方便用户使用，设计了一种ASTL模板来帮助用户准确地在ASTL公式中指定其监测需求（图2）。

（4）最后，在公开可用的数据集上进行了大量的实验，选取不同最先进方法与之对比，并探讨了不同影响因子的影响（图3-7）。实验结果表明，本研究工作所提出方法在资源动变的物联网网络中表现优于对比方法，具有更高的应用鲁棒性。

图1 物联网服务实时定量监测应用案例

图2 基于ASTL模板的物联网服务监测过程

图3 不同空间约束（处于、到达、规避特定区域）下不同对比方法的实验结果

图4 存储空间约束和空间约束多约束下不同物联网服务和不同对比方法的实验结果

图5 不同权重（系数衰减、倒数值、随机值）下的不同空间约束（规避、到达特定区域）的实时监测结果

图6 不同物联网服务在不同影响因子不同对比方法下的实验结果

图7 多约束下（同时满足、至少满足一个、不同约束个数）的实验结果

本研究受到国家重点研发计划（2018YFB1402800）和国家自然科学基金（42050103）联合资助。发表在国际权威期刊《IEEE Transactions on Mobile Computing》：Deng Zhao, Zhangbing Zhou, Zhipeng Cai, Sami Yangui, Xiao Xue. ASTL: Accumulative STL With a Novel Robustness Metric for IoT Service Monitoring [J]. IEEE Transactions on Mobile Computing, 2023, 22(10): 5751-5768.（中国计算机学会CCF A类期刊, 影响因子：7.9）

全文链接：https://ieeexplore.ieee.org/document/9785902