微信服务号

微信订阅号

2025-4-3- 19
Home > Archive>Volume 29, Issue 6, 2018 >1622-1634. DOI:10.13328/j.cnki.jos.005466
PDF HTML XML Export Cite reminder
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)

  • Article
    • | |
  • Metrics
    • |
  • Reference [32]
    • |
  • Related [20]
    • | | |
  • Comments
    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.

    Reference
    [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]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 01,2017
  • Revised:September 01,2017
  • Adopted:November 06,2017
  • Online: December 28,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2032434Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063