普适计算应用时空性质的运行时验证
作者:
作者单位:

作者简介:

李晅松(1985-),男,山东博兴人,博士,讲师,CCF专业会员,主要研究领域为软件工程与方法学,形式化方法,普适计算技术;陶先平(1970-),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为软件中间件技术,网构软件方法学,普适计算技术;宋巍(1981-),男,博士,副教授,CCF高级会员,主要研究领域为软件工程与方法学,形式化方法,服务计算.

通讯作者:

李晅松,E-mail:lixs@njust.edu.cn

中图分类号:

基金项目:

国家重点研发计划(2017YFB1001801);国家自然科学基金(61702263,61373011);江苏省自然科学基金(BK20171427);中央高校基本科研业务费专项资金(30917011322)


Runtime Verification of Spatio-Temporal Properties for Pervasive Computing Applications
Author:
Affiliation:

Fund Project:

National Key R&D Program of China (2017YFB1001801); National Natural Science Foundation of China(61702263, 61373011); Natural Science Foundation of Jiangsu Province (BK20171427); Fundamental Research Funds for the CentralUniversities (30917011322)

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

    运行时验证是提升普适计算应用可靠性的重要手段.这类应用的很多性质同时涉及时间关系和空间位置关系,这样的时空性质给运行时的验证带来了特有挑战:一方面,传统的时态逻辑难以描述空间性质;另一方面,适合描述空间性质的Ambient Logic在真值不确定等情况下不能很好地支持有限轨迹中时间性质的描述.为支持普适计算应用时空性质的运行时验证,引入三值逻辑语义,提出了AL3(3-valued ambient logic);并在此基础上设计实现了基于AL3的性质检验算法和运行时监控器.最后,通过案例分析和运行效率实验阐明了所提方法的有效性和可行性.

    Abstract:

    Runtime verification is an important method for improving software reliability of pervasive computing applications. Some properties of these applications consider both temporal and spatial relationships. Such spatio-temporal properties bring some specific challenges for runtime verification. On one hand, traditional temporal logic cannot describe spatial properties. On the other hand, while ambient logic is suitable for spatial properties, it does not properly support the description of temporal properties in finite traces, especially when the truth values cannot be decided. In order to support the runtime verification of spatio-temporal properties for pervasive computing applications, this paper firstly imports 3-valued semantics and proposes AL3 (3-valued ambient logic). On the basis of AL3, it designs and implements an algorithm for properties checking and a runtime monitor. Moreover, the paper uses a case study and a performance measurement to clarify the usability and feasibility of the proposed approach.

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

李晅松,陶先平,宋巍.普适计算应用时空性质的运行时验证.软件学报,2018,29(6):1622-1634

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

京公网安备 11040202500063号