微信服务号

微信订阅号

2025-4-9- 20
Home > Archive>Volume 28, Issue 5, 2017 >1167-1182. DOI:10.13328/j.cnki.jos.005215
PDF HTML XML Export Cite reminder
Specification and Runtime Verification for Activity-Oriented Context-Aware Applications
Author:
Affiliation:

Fund Project:

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

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

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

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

Copy
Share
Article Metrics
  • Abstract:4294
  • PDF: 6173
  • HTML: 3091
  • Cited by: 0
History
  • Received:July 15,2016
  • Revised:September 25,2016
  • Online: January 22,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2034202Visitors
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