IEICE TRANSACTIONS on Information
IoT Modeling and Verification: From the CaIT Calculus to UPPAAL
Summary :
With the support of emerging technologies such as 5G, machine learning, edge computing and Industry 4.0, the Internet of Things (IoT) continues to evolve and promote the construction of future networks. Existing work on IoT mainly focuses on its practical applications, but there is little research on modeling the interactions among components in IoT systems and verifying the correctness of the network deployment. Therefore, the Calculus of the Internet of Things (CaIT) has previously been proposed to formally model and reason about IoT systems. In this paper, the CaIT calculus is extended by introducing broadcast communications. For modeling convenience, we provide explicit operations to model node mobility as well as the interactions between sensors (or actuators) with the environment. To support the use of UPPAAL to verify the temporal properties of IoT networks described by the CaIT calculus, we establish a relationship between timed automata and the CaIT calculus. Using UPPAAL, we verify six temporal properties of a simple “smart home” example, including Boiler On Manually, Boiler Off Automatically, Boiler On Automatically, Lights On, Lights Mutually, and Windows Simultaneously. The verification results show that the “smart home” can work properly.
- Publication
- IEICE TRANSACTIONS on Information Vol.E106-D No.9 pp.1507-1518
- Publication Date
- 2023/09/01
- Publicized
- 2023/06/02
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.2022EDP7223
- Type of Manuscript
- PAPER
- Category
- Fundamentals of Information Systems
Authors
Ningning CHEN
East China Normal University
Huibiao ZHU
East China Normal University
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Ningning CHEN, Huibiao ZHU, "IoT Modeling and Verification: From the CaIT Calculus to UPPAAL" in IEICE TRANSACTIONS on Information,
vol. E106-D, no. 9, pp. 1507-1518, September 2023, doi: 10.1587/transinf.2022EDP7223.
Abstract: With the support of emerging technologies such as 5G, machine learning, edge computing and Industry 4.0, the Internet of Things (IoT) continues to evolve and promote the construction of future networks. Existing work on IoT mainly focuses on its practical applications, but there is little research on modeling the interactions among components in IoT systems and verifying the correctness of the network deployment. Therefore, the Calculus of the Internet of Things (CaIT) has previously been proposed to formally model and reason about IoT systems. In this paper, the CaIT calculus is extended by introducing broadcast communications. For modeling convenience, we provide explicit operations to model node mobility as well as the interactions between sensors (or actuators) with the environment. To support the use of UPPAAL to verify the temporal properties of IoT networks described by the CaIT calculus, we establish a relationship between timed automata and the CaIT calculus. Using UPPAAL, we verify six temporal properties of a simple “smart home” example, including Boiler On Manually, Boiler Off Automatically, Boiler On Automatically, Lights On, Lights Mutually, and Windows Simultaneously. The verification results show that the “smart home” can work properly.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2022EDP7223/_p
Copy
@ARTICLE{e106-d_9_1507,
author={Ningning CHEN, Huibiao ZHU, },
journal={IEICE TRANSACTIONS on Information},
title={IoT Modeling and Verification: From the CaIT Calculus to UPPAAL},
year={2023},
volume={E106-D},
number={9},
pages={1507-1518},
abstract={With the support of emerging technologies such as 5G, machine learning, edge computing and Industry 4.0, the Internet of Things (IoT) continues to evolve and promote the construction of future networks. Existing work on IoT mainly focuses on its practical applications, but there is little research on modeling the interactions among components in IoT systems and verifying the correctness of the network deployment. Therefore, the Calculus of the Internet of Things (CaIT) has previously been proposed to formally model and reason about IoT systems. In this paper, the CaIT calculus is extended by introducing broadcast communications. For modeling convenience, we provide explicit operations to model node mobility as well as the interactions between sensors (or actuators) with the environment. To support the use of UPPAAL to verify the temporal properties of IoT networks described by the CaIT calculus, we establish a relationship between timed automata and the CaIT calculus. Using UPPAAL, we verify six temporal properties of a simple “smart home” example, including Boiler On Manually, Boiler Off Automatically, Boiler On Automatically, Lights On, Lights Mutually, and Windows Simultaneously. The verification results show that the “smart home” can work properly.},
keywords={},
doi={10.1587/transinf.2022EDP7223},
ISSN={1745-1361},
month={September},}
Copy
TY - JOUR
TI - IoT Modeling and Verification: From the CaIT Calculus to UPPAAL
T2 - IEICE TRANSACTIONS on Information
SP - 1507
EP - 1518
AU - Ningning CHEN
AU - Huibiao ZHU
PY - 2023
DO - 10.1587/transinf.2022EDP7223
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E106-D
IS - 9
JA - IEICE TRANSACTIONS on Information
Y1 - September 2023
AB - With the support of emerging technologies such as 5G, machine learning, edge computing and Industry 4.0, the Internet of Things (IoT) continues to evolve and promote the construction of future networks. Existing work on IoT mainly focuses on its practical applications, but there is little research on modeling the interactions among components in IoT systems and verifying the correctness of the network deployment. Therefore, the Calculus of the Internet of Things (CaIT) has previously been proposed to formally model and reason about IoT systems. In this paper, the CaIT calculus is extended by introducing broadcast communications. For modeling convenience, we provide explicit operations to model node mobility as well as the interactions between sensors (or actuators) with the environment. To support the use of UPPAAL to verify the temporal properties of IoT networks described by the CaIT calculus, we establish a relationship between timed automata and the CaIT calculus. Using UPPAAL, we verify six temporal properties of a simple “smart home” example, including Boiler On Manually, Boiler Off Automatically, Boiler On Automatically, Lights On, Lights Mutually, and Windows Simultaneously. The verification results show that the “smart home” can work properly.
ER -
English
