微信服务号

微信订阅号

2025年4月26日 23:12 星期六
首页 > 过刊浏览>2018年第29卷第6期 >1622-1634. DOI:10.13328/j.cnki.jos.005466
PDF HTML阅读 XML下载 导出引用 引用提醒
普适计算应用时空性质的运行时验证
作者:
作者简介:

李晅松(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:
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)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [32]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    运行时验证是提升普适计算应用可靠性的重要手段.这类应用的很多性质同时涉及时间关系和空间位置关系，这样的时空性质给运行时的验证带来了特有挑战：一方面，传统的时态逻辑难以描述空间性质；另一方面，适合描述空间性质的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.

    参考文献
    [1] Weiser M. The computer for the 21st century. Scientific American, 1991,261(30):94-104.[doi:10.1145/329124.329126]
    [2] Satyanarayanan M. Pervasive computing:Vision and challenges. IEEE Personal Communications, 2001,8(4):10-17.[doi:10.1109/98.943998]
    [3] Dey AK, Abowd GD, Salber D. A conceptual framework and a toolkit for supporting the rapid prototyping of context-aware applications. Human-Computer Interaction, 2001,16(2):97-166.[doi:10.1207/S15327051HCI16234_02]
    [4] Román M, Hess C, Cerqueira R, Ranganathan A, Campbell RH, Nahrstedte K. A middleware infrastructure for active spaces. IEEE Pervasive Computing, 2002,1(4):74-83.[doi:10.1109/MPRV.2002.1158281]
    [5] Kulkarni D, Ahmed T, Tripathi A. A generative programming framework for context-aware CSCW applications. ACM Trans. on Software Engineering and Methodology (TOSEM), 2012,21(2):11.[doi:10.1145/2089116.2089121]
    [6] Gu T, Pung HK, Zhang DQ. Toward an OSGi-based infrastructure for context-aware applications. IEEE Pervasive Computing, 2004,3(4):66-74.[doi:10.1109/MPRV.2004.19]
    [7] Arcelus A, Jones MH, Goubran R, Knoefel F. Integration of smart home technologies in a health monitoring system for the elderly. In:Proc. of the 21st IEEE Int'l Conf. on Advanced Information Networking and Applications (AINA) Workshops. 2007. 820-825.[doi:10.1109/AINAW.2007.209]
    [8] Julien C, Roman GC. Egospaces:Facilitating rapid development of context-aware mobile applications. IEEE Trans. on Software Engineering (TSE), 2006,32(5):281-298.[doi:10.1109/TSE.2006.47]
    [9] Artho C, Barringer H, Goldberg A, Havelund K, Khurshid S, Lowry M, Pasareanu C, Rosu G, Sen K, Visser W. Combining test case generation and runtime verification. Theoretical Computer Science (TCS), 2005,336(2):209-234.[doi:10.1016/j.tcs.2004.11. 007]
    [10] Zhang X, Dong W, Qi ZC. Conflicts detection in runtime verification based on AOP. Ruan Jian Xue Bao/Journal of Software, 2011, 22(6):1224-1235(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4016.htm[doi:10.3724/SP.J.1001.2011. 04016]
    [11] Bakhouya M, Campbell R, Coronato A, De Pietro G, Ranganathan A. Introduction to special section on formal methods in pervasive computing. ACM Trans. on Autonomous and Adaptive Systems (TAAS), 2012,7(1):6.[doi:10.1145/2168260.2168266]
    [12] Ranganathan A, Campbell RH. An infrastructure for context-awareness based on first order logic. Personal and Ubiquitous Computing (PUC), 2003,7(6):353-364.[doi:10.1007/s00779-003-0251-x]
    [13] Pnueli A. The temporal logic of programs. In:Proc. of 18th Annual Symp. on Foundations of Computer Science. IEEE, 1977. 46-57.[doi:10.1109/SFCS.1977.32]
    [14] Emerson EA, Halpern JY. Decision procedures and expressiveness in the temporal logic of branching time. In:Proc. of the 14th Annual ACM Symp. on Theory of Computing. ACM Press, 1982. 169-180.[doi:10.1145/800070.802190]
    [15] Cardelli L, Gordon AD. Mobile ambients. In:Proc. of the Int'l Conf. on Foundations of Software Science and Computation Structure. Springer Berlin Heidelberg, 1998. 140-155.[doi:10.1007/BFb0053547]
    [16] Cardelli L, Gordon AD. Ambient logic. In:Proc. of the Mathematical Structures in Computer Science. 2003.
    [17] Ranganathan A, Campbell RH. Provably correct pervasive computing environments. In:Proc. of the 6th IEEE Int'l Conf. on Pervasive Computing and Communications (PerCom). 2008. 160-169.[doi:10.1109/PERCOM.2008.116]
    [18] Coronato A, De Pietro G. Formal specification of wireless and pervasive healthcare applications. ACM Trans. on Embedded Computing Systems (TECS), 2010,10(1):12.[doi:10.1145/1814539.1814551]
    [19] Li XS, Tao XP, Lü J, Song W. Specification and runtime verification for activity-oriented context-aware applications. Ruan Jian Xue Bao/Journal of Software, 2017,28(5):1167-1182(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5215.htm[doi:10.13328/j.cnki.jos.005215]
    [20] Bauer A, Leucker M, Schallhart C. Runtime verification for LTL and TLTL. ACM Trans. on Software Engineering and Methodology (TOSEM), 2011,20(4):14.[doi:10.1145/2000799.2000800]
    [21] Charatonik W, Zilio SD, Gordon AD, Mukhopadhyay S, Talbot J. Model checking mobile ambients. Theoretical Computer Science, 2003,308(1-3):277-331.[doi:10.1016/S0304-3975(02)00832-0]
    [22] Li XS, Tao XP, Lü J. Programming method and formalization for activity-oriented context-aware applications. In:Proc. of the 12th Int'l Conf. on Ubiquitous Intelligence and Computing (UIC). IEEE, 2015. 174-181.[doi:10.1109/UIC-ATC-ScalCom-CBDComIoP.2015.48]
    [23] Wei H, Huang Y, Cao J, Ma XX, Lü J. Formal specification and runtime detection of temporal properties for asynchronous context. In:Proc. of the 10th Int'l Conf. on Pervasive Computing and Communications (PerCom). IEEE, 2012. 30-38.[doi:10.1109/PerCom.2012.6199846]
    [24] Kleene S. Introduction to Metamathematics. Wolters-Noordhoff, 1971.
    [25] Jiang Y, Liu H, Kong H, Wang R, Hosseini M, Sun J, Sha L. Use runtime verification to improve the quality of medical care practice. In:Proc. of the 38th IEEE/ACM Int'l Conf. on Software Engineering Companion. ACM Press, 2016. 112-121.
    [26] Kane A, Chowdhury O, Datta A, Koopman P. A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In:Proc. of the 6th Int'l Conf. on Runtime Verification. LNCS 9333. Springer Int'l Publishing, 2015. 102-117.[doi:10. 1007/978-3-319-23820-3_7]
    [27] Yu K, Chen Z, Dong W. A predictive runtime verification framework for cyber-physical systems. In:Proc. of the 8th IEEE Int'l Conf. on Software Security and Reliability-Companion. IEEE, 2014. 223-227.[doi:10.1109/SERE-C.2014.43]
    [28] Zhou J, Chen Z, Wang J, Zheng Z, Dong W. A runtime verification based trace-oriented monitoring framework for cloud systems. In:Proc. of IEEE Int'l Symp. on Software Reliability Engineering Workshops. IEEE, 2014. 152-155.[doi:10.1109/ISSREW.2014. 84]
    [29] Bruns G, Godefroid P. Model checking partial state spaces with 3-valued temporal logics. In:Proc. of the Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg:Springer-Verlag, 1999. 274-287.[doi:10.1007/3-540-48683-6_25]
    附中文参考文献:
    [10] 张献,董威,齐治昌.基于AOP的运行时验证中的冲突检测.软件学报,2011,22(6):1224-1235. http://www.jos.org.cn/1000-9825/4016.htm[doi:10.3724/SP.J.1001.2011.04016]
    [19] 李晅松,陶先平,吕建,宋巍.面向动作的上下文感知应用的规约与运行时验证.软件学报,2017,28(5):1167-1182. http://www.jos. org.cn/1000-9825/5215.htm[doi:10.13328/j.cnki.jos.005215]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2017-07-01
  • 最后修改日期:2017-09-01
  • 录用日期:2017-11-06
  • 在线发布日期: 2017-12-28
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19877027位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号