Modeling and Verification for Mobile and Communication Behaviors of IoT Devices
Author:
Affiliation:

Clc Number:

TP311

  • Article
  • | |
  • Metrics
  • |
  • Reference [30]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    The utilization range of Internet of Things (IoT) devices is expanding. Model checking is an effective approach to improve the reliability and security of such devices. However, the commonly adopted model checking methods cannot well describe the cross-space movement and communication behavior common in such devices. To this end, this study proposes a modeling and verification method for the mobile and communication behavior of IoT devices to verify their spatio-temporal properties. Additionally, push/pull action and global communication mechanism are integrated into ambient calculus to propose the ambient calculus with global communication (ACGC) and provide a model checking algorithm for ACGC against the ambient logic. Then, the modeling language for mobility and communication (MLMC) is put forward to describe mobile and communication behavior of IoT devices. Additionally, a method to convert the MLMC-based description into an ACGC model is given. Furthermore, a model checking tool ACGCCk is implemented to verify whether the properties of IoT devices are satisfied. Meanwhile, some optimizations are conducted to accelerate the checking. Finally, the effectiveness of the proposed method is demonstrated by case study and experimental analysis.

    Reference
    [1] IoT Analytics. IoT 2021 in review: The 10 most relevant IoT developments of the year. 2021. https://iot-analytics.com/iot-2021-in-review/
    [2] Pnueli A. The temporal logic of programs. In: Proc. of the 18th Annual Symp. on Foundations of Computer Science. Providence: IEEE, 1977. 46–57.
    [3] Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. of the Workshop on Logic of Programs. Yorktown Heights: Springer, 1981. 52–71.
    [4] Cardelli L, Gordon AD. Anytime, anywhere: Modal logics for mobile ambients. In: Proc. of the 27th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Boston: ACM, 2000. 365–377.
    [5] Cardelli L, Gordon AD. Mobile ambients. In: Proc. of the 1st Int’l Conf. on Foundations of Software Science and Computation Structure. Lisbon: Springer, 1998. 140–155.
    [6] Levi F, Sangiorgi D. Mobile safe ambients. ACM Trans. on Programming Languages and Systems, 2003, 25(1): 1–69.
    [7] Bugliesi M, Castagna G, Crafa S. Boxed ambients. In: Proc. of the 4th Int’l Symp. on Theoretical Aspects of Computer Software. Sendai: Springer, 2001. 38–63.
    [8] Phillips I, Vigliotti MG. On reduction semantics for the push and pull ambient calculus. In: Baeza-Yates R, Montanari U, Santoro N, eds. Foundations of Information Technology in the Era of Network and Mobile Computing. Boston: Springer, 2002. 550–562.
    [9] Gul N. A calculus of mobility and communication for ubiquitous computing [Ph.D. Thesis]. Leicester: University of Leicester, 2015.
    [10] Milner R. Communicating and Mobile Systems: the π-Calculus. Cambridge: Cambridge University Press, 1999. 75–156.
    [11] Charatonik W, Dal Zilio S, Gordon AD, Mukhopadhyay S, Talbot JM. Model checking mobile ambients. Theoretical Computer Science, 2003, 308(1–3): 277–331.
    [12] Nielson F, Nielson HR, Sagiv M. A kleene analysis of mobile ambients. In: Proc. of the 9th European Symp. on Programming. Berlin: Springer, 2000. 305–319.
    [13] 刘熙旺, 李良, 郭雅萍, 章飞. 电梯及机器人乘梯的方法和装置. CN108163653B, 2020-08-18.
    Liu XW, Li L, Guo YP, Zhang F. Method and device for elevator and robot riding. CN108163653B. 2020-08-18 (in Chinese).
    [14] Ichinose R, Takeuchi I, Teramoto T. Elevator system that autonomous mobile robot takes together with person: US, 8958910B2, 2015-02-17.
    [15] Lin HM. Predicate μ-calculus for mobile ambients. Journal of Computer Science and Technology, 2005, 20(1): 95–104.
    [16] 江华. 界程演算模型检测 [博士学位论文]. 贵阳: 贵州大学, 2008.
    Jiang H. Model checking for mobile ambients [Ph.D. Thesis]. Guiyang: Guizhou University, 2008 (in Chinese with English abstract).
    [17] 林荣德. 移动界程演算及模型检测应用的关键问题研究 [博士学位论文]. 广州: 华南理工大学, 2010.
    Lin RD. Research on key issues of mobile ambients and model checking applications [Ph.D. Thesis]. Guangzhou: South China University of Technology, 2010 (in Chinese with English abstract).
    [18] 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.
    [19] Kato T, Miyai A, Higuchi M. IDE for the ambient calculus in distributed environments. In: Proc. of the 2014 Int’l Conf. on Industrial Automation, Information and Communications Technology. Bali: IEEE, 2014. 83–89. [doi: 10.1109/IAICT.2014.6922104]
    [20] 李晅松, 陶先平, 吕建, 宋巍. 面向动作的上下文感知应用的规约与运行时验证. 软件学报, 2017, 28(5): 1167–1182. http://www.jos.org.cn/1000-9825/5215.htm
    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
    [21] Zhang LF, He WJ, Martinez J, Brackenbury N, Lu S, Ur B. AutoTap: Synthesizing and repairing trigger-action programs using LTL properties. In: Proc. of the 41st IEEE/ACM Int’l Conf. on Software Engineering. Montreal: IEEE, 2019. 281–291.
    [22] Wang Q, Datta P, Yang W, Liu S, Bates A, Gunter CA. Charting the attack surface of trigger-action IoT platforms. In: Proc. of the 2019 ACM SIGSAC Conf. on Computer and Communications Security. London: ACM, 2019. 1439–1453. [doi: 10.1145/3319535.3345662]
    [23] Celik ZB, McDaniel PD, Tan G. Soteria: Automated IoT safety and security analysis. In: Proc. of the 2018 USENIX Annual Technical Conf. Boston: USENIX Association, 2018. 147–158.
    [24] Bu L, Xiong W, Liang CJM, Han S, Zhang DM, Lin S, Li XD. Systematically ensuring the confidence of real-time home automation IoT systems. ACM Trans. on Cyber-physical Systems, 2018, 2(3): 22.
    [25] Ranganathan A, Campbell RH. Provably correct pervasive computing environments. In: Proc. of the 6th IEEE Int’l Conf. on Pervasive Computing and Communications. Hong Kong: IEEE, 2008. 160–169. [doi: 10.1109/PERCOM.2008.116]
    [26] Li XS, Tao XP, Lu J. Programming method and formalization for activity-oriented context-aware applications. In: Proc. of the 12th Int’l Conf. on Ubiquitous Intelligence and Computing and the 12th Int’l Conf. on Autonomic and Trusted Computing and the 15th IEEE Int’l Conf. on Scalable Computing and Communications and its Associated Workshops. Beijing: IEEE, 2015. 174–181.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

刘靖宇,李晅松,陈芝菲,叶海波,宋巍.面向物联网设备移动与通信行为的建模及验证.软件学报,2024,35(11):4993-5015

Copy
Share
Article Metrics
  • Abstract:497
  • PDF: 1982
  • HTML: 496
  • Cited by: 0
History
  • Received:September 18,2022
  • Revised:May 07,2023
  • Online: February 05,2024
  • Published: November 06,2024
You are the first2031526Visitors
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