TY - GEN
T1 - Denotational and Algebraic Semantics for the CaIT Calculus
AU - Chen, Ningning
AU - Zhu, Huibiao
N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2022
Y1 - 2022
N2 - The Internet of Things (IoT) has been wildly used in various fields of our lives, such as health care, smart environment, transportation, etc. However, the existing research on IoT mainly concentrates on its practical applications, and there is still a lack of work on modelling and reasoning about IoT systems from the perspective of formal methods. Therefore, the Calculus of the Internet of Things (CaIT) has been proposed to model the interactions among components and verify the network deployment to ensure the quality and reliability of IoT systems. Unfortunately, the CaIT calculus can only support point-to-point communication, while broadcast communication is more common in IoT systems. Therefore, this paper updates the CaIT calculus by replacing its communication primitive with the broadcast. Based on the Unifying Theories of Programming (UTP), we further explore its denotational semantics and algebraic semantics, with a special focus on broadcast communication, actions with the timeout (e.g. input actions and migration actions), and channel restriction. To facilitate the algebraic exploration of parallel expansion laws, we further extend the CaIT calculus with a new concept called guarded choice, which allows us to transform each program into the guarded choice form.
AB - The Internet of Things (IoT) has been wildly used in various fields of our lives, such as health care, smart environment, transportation, etc. However, the existing research on IoT mainly concentrates on its practical applications, and there is still a lack of work on modelling and reasoning about IoT systems from the perspective of formal methods. Therefore, the Calculus of the Internet of Things (CaIT) has been proposed to model the interactions among components and verify the network deployment to ensure the quality and reliability of IoT systems. Unfortunately, the CaIT calculus can only support point-to-point communication, while broadcast communication is more common in IoT systems. Therefore, this paper updates the CaIT calculus by replacing its communication primitive with the broadcast. Based on the Unifying Theories of Programming (UTP), we further explore its denotational semantics and algebraic semantics, with a special focus on broadcast communication, actions with the timeout (e.g. input actions and migration actions), and channel restriction. To facilitate the algebraic exploration of parallel expansion laws, we further extend the CaIT calculus with a new concept called guarded choice, which allows us to transform each program into the guarded choice form.
KW - Algebraic semantics
KW - Denotational semantics
KW - IoT
KW - The CaIT calculus
KW - UTP
UR - https://www.scopus.com/pages/publications/85140714515
U2 - 10.1007/978-3-031-17715-6_10
DO - 10.1007/978-3-031-17715-6_10
M3 - 会议稿件
AN - SCOPUS:85140714515
SN - 9783031177149
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 132
EP - 150
BT - Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings
A2 - Seidl, Helmut
A2 - Liu, Zhiming
A2 - Pasareanu, Corina S.
PB - Springer Science and Business Media Deutschland GmbH
T2 - 19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022
Y2 - 27 September 2022 through 29 September 2022
ER -