A proof system of the CaIT calculus

Abstract

The Internet of Things (IoT) can realize the interconnection of people, machines, and things anytime, anywhere. Most of the existing research mainly focuses on the practical applications of IoT, and there is a lack of research on modeling and reasoning about IoT systems from the perspective of formal methods. Thus, the Calculus of the Internet of Things (CaIT) has been proposed to specify and analyze IoT systems before the actual implementation, which can effectively improve development efficiency, and enhance system quality and reliability. To verify the correctness of IoT systems described by CaIT, this paper presents a proof system for CaIT, in which specifications and verifications are based on the extended Hoare Logic with time. Furthermore, we explore the cooperation between isolated proofs to validate the postconditions of the communication actions occurring in these proofs, with a particular focus on broadcast communication. We also demonstrate the soundness of our proof system. A simple “smart home” is given to illustrate the availability of our proof system.

Graphical abstract

Keywords

Internet of Things (IoT) / Calculus of the Internet of Things (CaIT) / extended hoare logic / cooperation / smart home

Ningning Chen is currently a PhD candidate in Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, China. Her research interests contain Hoare logic, formal methods, process algebra and IoT

Huibiao Zhu is currently a professor in East China Normal University, China. He earned his PhD degree in formal methods from London South Bank University, UK in 2005. During these years, he has studied various semantics and their linking theories for Verilog, SystemC, Web services and probability system. He was the Chinese PI of the Sino-Danish Basic Research Center IDEA4CPS

References

[1] Ashton K. That “internet of things” thing. RFID Journal, 2009, 22(7): 97−114

[2] Gubbi J, Buyya R, Marusic S, Palaniswami M . Internet of things (IoT): a vision, architectural elements, and future directions. Future Generation Computer Systems, 2013, 29( 7): 1645–1660

[3] Zhang Y. Technology framework of the internet of things and its application. In: Proceedings of 2011 International Conference on Electrical and Control Engineering. 2011, 4109−4112

[4] Atzori L, Iera A, Morabito G . The internet of things: a survey. Computer Networks, 2010, 54( 15): 2787–2805

[5] Hosseinzadeh M, Tho Q T, Ali S, Rahmani A M, Souri A, Norouzi M, Huynh B . A hybrid service selection and composition model for cloud-edge computing in the internet of things. IEEE Access, 2020, 8: 85939–85949

[6] Harbi Y, Aliouat Z, Refoufi A, Harous S . Recent security trends in internet of things: a comprehensive survey. IEEE Access, 2021, 9: 113292–113314

[7] Nienhuis K, Joannou A, Bauereiss T, Fox A, Roe M, Campbell B, Naylor M, Norton R M, Moore S W, Neumann P G, Stark I, Watson R N M, Sewell P. Rigorous engineering for hardware security: formal modelling and proof in the CHERI design and implementation process. In: Proceedings of 2020 IEEE Symposium on Security and Privacy. 2020, 1003−1020

[8] Asavoae M, Haur I, Jan M, Ben Hedia B, Schoeberl M. Towards formal co-validation of hardware and software timing models of CPSs. In: Proceedings of the 9th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems. 2019, 203−227

[9] Schmidt B. Programmnetzlisten: Ein formales Modell fur die Verifikation von Hardwarenaher Software in Eingebetteten Systemen. Technische Universitat Kaiserslautern, Dissertation, 2020

[10] Lanese I, Bedogni L, Di Felice M. Internet of things: a process calculus approach. In: Proceedings of the 28th Annual ACM Symposium on Applied Computing. 2013, 1339−1346

[11] Bodei C, Degano P, Ferrari G L, Galletta L. Where do your IoT ingredients come from? In: Proceedings of the 18th International Conference on Coordination Languages and Models. 2016, 35–50

[12] Lanotte R, Merro M . A semantic theory of the internet of things. Information and Computation, 2018, 259: 72–101

[13] Apt K R, Olderog E R, Apt K R. Verification of Sequential and Concurrent Programs. 3rd ed. New York: Springer, 2009

[14] Hooman J. Compositional verification of real-time systems using extended Hoare triples. In: Proceedings of the Real-Time: Theory in Practice, REX Workshop. 1991, 252−290

[15] Hooman J . Extending Hoare logic to real-time. Formal Aspects of Computing, 1994, 6( S1): 801–825

[16] Akyildiz I F, Jornet J M, Han C . Terahertz band: next frontier for wireless communications. Physical Communication, 2014, 12: 16–32

[17] van der Heijden F, Duin R P W, De Ridder D, Tax D M J. Classification, Parameter Estimation and State Estimation: an Engineering Approach Using MATLAB. Chichester: John Wiley & Sons, ltd., 2004

[18] Prasad K V S. A calculus of broadcasting systems. Science of Computer Programming, 1995, 25(2–3): 2–3

[19] Nanz S, Hankin C. A framework for security analysis of mobile wireless networks. Theoretical Computer Science, 2006, 367(1–2): 1–2

[20] Merro M . An observational theory for mobile ad hoc networks (full version). Information and Computation, 2009, 207( 2): 194–208

[21] Hoare C A R . An axiomatic basis for computer programming. Communications of the ACM, 1969, 12( 10): 576–580

[22] Barthe G, Gaboardi M, Arias E J G, Hsu J, Kunz C, Strub P Y. Proving differential privacy in Hoare logic. In: Proceedings of the 27th IEEE Computer Security Foundations Symposium. 2014, 411−424

[23] Arthan R, Martin U, Oliva P . A Hoare logic for linear systems. Formal Aspects of Computing, 2013, 25( 3): 345–363

[24] Luo C, Qin S, Qiu Z . Verifying BPEL-like programs with Hoare logic. Frontiers of Computer Science in China, 2008, 2( 4): 344–356

[25] de Boer F S. A Hoare logic for dynamic networks of asynchronously communicating deterministic processes. Theoretical Computer Science, 2002, 274(1–2): 1–2

[26] Apt K R, Francez N, de Roever W P . A proof system for communicating sequential processes. ACM Transactions on Programming Languages and Systems, 1980, 2( 3): 359–385

[27] Hoare C A R, He J. Unifying Theories of Programming. London: Prentice Hall, 1998

[28] Paulson L C. Isabelle: a Generic Theorem Prover. Berlin: Springer, 1994

[29] Huet G, Kahn G, Paulin-Mohring C. The coq proof assistant: a tutorial. Rapport Technique, 1997, 178

Acknowledgements

This work was partially supported by the National Key Research and Development Program of China (No. 2022YFB3305102), the National Natural Science Foundation of China (Grant Nos. 62032024, 61872145), the “Digital Silk Road” Shanghai International Joint Lab of Trustworthy Intelligent Software (No. 22510750100)， Shanghai Trusted Industry Internet Software Collaborative Innovation Center, and the Dean’s Fund of Shanghai Key Laboratory of Trustworthy Computing (East China Normal University).

RIGHTS & PERMISSIONS

2024 Higher Education Press