微信服务号

微信订阅号

2025年6月1日 18:27 星期日
首页 > 过刊浏览>2017年第28卷第5期 >1167-1182. DOI:10.13328/j.cnki.jos.005215
PDF HTML阅读 XML下载 导出引用 引用提醒
面向动作的上下文感知应用的规约与运行时验证
作者:
基金项目:

国家自然科学基金（61373011，61202003，61502225）


Specification and Runtime Verification for Activity-Oriented Context-Aware Applications
Author:
Fund Project:

National Natural Science Foundation of China (61373011, 61202003, 61502225)

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

    面向动作的上下文感知（activity-oriented context-aware，简称AOCA）应用组织环境中的资源，为用户动作的顺利进行提供支持.为应对环境和动作相关需求的开放性，这类应用采用轻量级、增量式的开发方法进行开发.相对于在开发阶段描述全局信息的开发方法，AOCA应用的开发可能由不同开发者在不同时间共同参与，这可能会导致较多的不一致等问题，且难以在开发阶段被发现.围绕使用运行时验证手段提高AOCA应用可靠性这一目标展开研究.给出了对于AOCA应用运行状态进行形式化规约、对于系统级和应用级性质进行描述的方法.进一步地设计实现了AOCA应用监控器.最后，通过案例分析以及性能评估证实了该方法的有效性.

    Abstract:

    Activity-Oriented context-aware (AOCA) applications organize environment resources to support the smooth performing of user activities. These applications are developed with a light-weight and incremental method in order to deal with the openness of the environment and requirements related to user activities. In contrast to the methods which attempt to deal with information from an overall level, AOCA applications allow different developers take part in the development in different time. However, this method may lead to more problems such as inconsistency. These problems are difficult to be detected in the development phase. This study focuses on using runtime verification to enhance the reliability of AOCA applications. In this paper, a method is first proposed for specifying AOCA application runtime status and describing system-level and application-level properties. Next, an AOCA application monitor is designed and implemented. Moreover, a case study and a performance evaluation are described to demonstrate the usability of this method.

    参考文献
    [1] Weiser M. The computer for the 21st century. Scientific American, 1991,261(30):94-104.
    [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] Gu T, Pung HK, Zhang DQ. A service-oriented middleware for building context-aware services. Journal of Network and Computer Applications, 2005,28(1):1-18. [doi: 10.1016/j.jnca.2004.06.002]
    [5] Li XS. Research on technologies of design and implementation for activity-oriented context-aware (AOCA) application systems [Ph.D. Thesis]. Nanjing: Nanjing University, 2016 (in Chinese with English abstract).
    [6] 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]
    [7] 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]
    [8] Wang L, Gu T, Tao X, Chen H, Lü J. Recognizing multi-user activities using wearable sensors in a smart home. Pervasive and Mobile Computing, 2011,7(3):287-298. [doi: 10.1016/j.pmcj.2010.11.008]
    [9] Cardelli L, Gordon AD. Mobile ambients. In: Proc. of the Int'l Conf. on Foundations of Software Science and Computation Structure. Berlin, Heidelberg: Springer-Verlag, 1998. 140-155. [doi: 10.1007/BFb0053547]
    [10] 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]
    [11] Cardelli L, Gordon AD. Ambient logic. In: Mathematical Structures in Computer Science. 2003.
    [12] Baier C, Katoen JP, Larsen KG. Principles of Model Checking. MIT Press, 2008. 673-744.
    [13] Pnueli A. The temporal logic of programs. In: Proc. of the 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, 1982. 169-180. [doi: 10.1145/800070.802190]
    [15] 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]
    [16] 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, 2016. 112-121. [doi: 10.1145/ 2889160.2889233]
    [17] 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. Runtime Verification. LNCS 9333, Springer Int'l Publishing, 2015. 102-117. [doi: 10.1007/ 978-3-319-23820-3_7]
    [18] Anagnostopoulos CB, Ntarladimas Y, Hadjiefthymiades S. Situational computing: An innovative architecture with imprecise reasoning. Journal of Systems and Software, 2007,80(12):1993-2014. [doi: 10.1016/j.jss.2007.03.003]
    [19] Konur S, Fisher M, Dobson S, Knox S. Formal verification of a pervasive messaging system. Formal Aspects of Computing, 2014, 26(4):677-694. [doi: 10.1007/s00165-013-0277-4]
    [20] Schmidtke HR, Woo W. Towards ontology-based formal verification methods for context aware systems. In: Proc. of the 7th Int'l Conf. on Pervasive Computing. LNCS 5538, Berlin, Heidelberg: Springer-Verlag, 2009. 309-326. [doi: 10.1007/978-3-642-01516- 8_21]
    [21] Ranganathan A, Campbell RH. Provably correct pervasive computing environments. In: Proc. of the 6th IEEE Int'l Conf. on Pervasive Computing and Communications. IEEE, 2008. 160-169. [doi: 10.1109/PERCOM.2008.116]
    [22] Coronato A, De Pietro G. Formal specification of wireless and pervasive healthcare applications. ACM Trans. on Embedded Computing Systems (TECS), 2010,10(1):12:1-12:18. [doi: 10.1145/1814539.1814551]
    [23] Weis T, Becker C, Brändle A. Towards a programming paradigm for pervasive applications based on the ambient calculus. In: Proc. of the Int'l Workshop on Combining Theory and Systems Building in Pervasive Computing (CTSB). 2006.
    [24] Coronato A, De Pietro G. Tools for the rapid prototyping of provably correct ambient intelligence applications. IEEE Trans. on Software Engineering, 2012,38(4):975-991. [doi: 10.1109/TSE.2011.67]
    [25] 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. IEEE, 2015. 174-181. [doi: 10.1109/UIC-ATC-ScalCom-CBDCom-IoP. 2015.48]
    [26] Song W, Ma XX, Hu H, Lü J. Dynamic evolution of processes in process-aware information systems. Ruan Jian Xue Bao/Journal of Software, 2011,22(3):417-438 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3962.htm [doi: 10.3724/SP.J. 1001.2011.03962]
    附中文参考文献:
    [5] 李晅松.面向动作的上下文感知应用系统的设计与实现技术研究[博士学位论文].南京:南京大学,2016.
    [7] 张献,董威,齐治昌.基于AOP的运行时验证中的冲突检测.软件学报,2011,22(6):1224-1235. http://www.jos.org.cn/1000- 9825/4016.htm [doi: 10.3724/SP.J.1001.2011.04016]
    [26] 宋巍,马晓星,胡昊,吕建.过程感知信息系统中过程的动态演化.软件学报,2011,22(3):417-438. http://www.jos.org.cn/1000- 9825/3962.htm [doi: 10.3724/SP.J.1001.2011.03962]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

李晅松,陶先平,吕建,宋巍.面向动作的上下文感知应用的规约与运行时验证.软件学报,2017,28(5):1167-1182

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

京公网安备 11040202500063号