Towards Formal Verification of Node RED-Based IoT Applications

Ikram Garfatta; Nour Elhouda Souid; Kaïs Klai

doi:10.1007/978-3-031-49737-7_7

Towards Formal Verification of Node RED-Based IoT Applications

Ikram Garfatta
, Nour Elhouda Souid
, Kaïs Klai

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

The world has been witnessing a proliferation of Internet of Things (IoT) applications in the last decade thanks to the growing awareness of the opportunities they can bring in various domains. However, the widespread adoption of IoT technologies highlights the importance of ensuring the correctness of these applications, which can have an impact on their security and reliability. The work presented in this paper contributes to the efforts addressing the verification in IoT. In this work, we are particularly interested in IoT applications developed using Node-RED, which despite being one of the most used tools by the IoT community still lacks attention when it comes to formal verification of its applications’ correctness and security. We therefore propose a first step towards a formal approach based on the formalization of IoT applications modeled with Node-RED flows that permits their formal verification. This step consists in formally defining Node-RED concepts and proposing a semantically equivalent Petri net model that would serve as a starting point for the development of a model-checker for Node-RED applications.

Original language	English
Title of host publication	Verification and Evaluation of Computer and Communication Systems - 16th International Conference, VECoS 2023, Proceedings
Editors	Belgacem Ben Hedia, Yassine Maleh, Moez Krichen
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	90-104
Number of pages	15
ISBN (Print)	9783031497360
DOIs	https://doi.org/10.1007/978-3-031-49737-7_7
Publication status	Published - 1 Jan 2024
Event	16th International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS 2023 - Marrakech, Morocco Duration: 18 Oct 2023 → 20 Oct 2023

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14368 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	16th International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS 2023
Country/Territory	Morocco
City	Marrakech
Period	18/10/23 → 20/10/23

Keywords

Formal Verification
Internet of Things
Node-RED
Petri nets

Access to Document

10.1007/978-3-031-49737-7_7

Cite this

Garfatta, I., Souid, N. E., & Klai, K. (2024). Towards Formal Verification of Node RED-Based IoT Applications. In B. Ben Hedia, Y. Maleh, & M. Krichen (Eds.), Verification and Evaluation of Computer and Communication Systems - 16th International Conference, VECoS 2023, Proceedings (pp. 90-104). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14368 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-49737-7_7

Garfatta, Ikram ; Souid, Nour Elhouda ; Klai, Kaïs. / Towards Formal Verification of Node RED-Based IoT Applications. Verification and Evaluation of Computer and Communication Systems - 16th International Conference, VECoS 2023, Proceedings. editor / Belgacem Ben Hedia ; Yassine Maleh ; Moez Krichen. Springer Science and Business Media Deutschland GmbH, 2024. pp. 90-104 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{a9c4ed85ff1a4b1b824cfee48bec6714,

title = "Towards Formal Verification of Node RED-Based IoT Applications",

abstract = "The world has been witnessing a proliferation of Internet of Things (IoT) applications in the last decade thanks to the growing awareness of the opportunities they can bring in various domains. However, the widespread adoption of IoT technologies highlights the importance of ensuring the correctness of these applications, which can have an impact on their security and reliability. The work presented in this paper contributes to the efforts addressing the verification in IoT. In this work, we are particularly interested in IoT applications developed using Node-RED, which despite being one of the most used tools by the IoT community still lacks attention when it comes to formal verification of its applications{\textquoteright} correctness and security. We therefore propose a first step towards a formal approach based on the formalization of IoT applications modeled with Node-RED flows that permits their formal verification. This step consists in formally defining Node-RED concepts and proposing a semantically equivalent Petri net model that would serve as a starting point for the development of a model-checker for Node-RED applications.",

keywords = "Formal Verification, Internet of Things, Node-RED, Petri nets",

author = "Ikram Garfatta and Souid, \{Nour Elhouda\} and Ka{\"i}s Klai",

note = "Publisher Copyright: {\textcopyright} 2024, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 16th International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS 2023 ; Conference date: 18-10-2023 Through 20-10-2023",

year = "2024",

month = jan,

day = "1",

doi = "10.1007/978-3-031-49737-7\_7",

language = "English",

isbn = "9783031497360",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "90--104",

editor = "\{Ben Hedia\}, Belgacem and Yassine Maleh and Moez Krichen",

booktitle = "Verification and Evaluation of Computer and Communication Systems - 16th International Conference, VECoS 2023, Proceedings",

}

Garfatta, I, Souid, NE & Klai, K 2024, Towards Formal Verification of Node RED-Based IoT Applications. in B Ben Hedia, Y Maleh & M Krichen (eds), Verification and Evaluation of Computer and Communication Systems - 16th International Conference, VECoS 2023, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14368 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 90-104, 16th International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS 2023, Marrakech, Morocco, 18/10/23. https://doi.org/10.1007/978-3-031-49737-7_7

Towards Formal Verification of Node RED-Based IoT Applications. / Garfatta, Ikram; Souid, Nour Elhouda; Klai, Kaïs.
Verification and Evaluation of Computer and Communication Systems - 16th International Conference, VECoS 2023, Proceedings. ed. / Belgacem Ben Hedia; Yassine Maleh; Moez Krichen. Springer Science and Business Media Deutschland GmbH, 2024. p. 90-104 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14368 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Towards Formal Verification of Node RED-Based IoT Applications

AU - Garfatta, Ikram

AU - Souid, Nour Elhouda

AU - Klai, Kaïs

PY - 2024/1/1

Y1 - 2024/1/1

N2 - The world has been witnessing a proliferation of Internet of Things (IoT) applications in the last decade thanks to the growing awareness of the opportunities they can bring in various domains. However, the widespread adoption of IoT technologies highlights the importance of ensuring the correctness of these applications, which can have an impact on their security and reliability. The work presented in this paper contributes to the efforts addressing the verification in IoT. In this work, we are particularly interested in IoT applications developed using Node-RED, which despite being one of the most used tools by the IoT community still lacks attention when it comes to formal verification of its applications’ correctness and security. We therefore propose a first step towards a formal approach based on the formalization of IoT applications modeled with Node-RED flows that permits their formal verification. This step consists in formally defining Node-RED concepts and proposing a semantically equivalent Petri net model that would serve as a starting point for the development of a model-checker for Node-RED applications.

AB - The world has been witnessing a proliferation of Internet of Things (IoT) applications in the last decade thanks to the growing awareness of the opportunities they can bring in various domains. However, the widespread adoption of IoT technologies highlights the importance of ensuring the correctness of these applications, which can have an impact on their security and reliability. The work presented in this paper contributes to the efforts addressing the verification in IoT. In this work, we are particularly interested in IoT applications developed using Node-RED, which despite being one of the most used tools by the IoT community still lacks attention when it comes to formal verification of its applications’ correctness and security. We therefore propose a first step towards a formal approach based on the formalization of IoT applications modeled with Node-RED flows that permits their formal verification. This step consists in formally defining Node-RED concepts and proposing a semantically equivalent Petri net model that would serve as a starting point for the development of a model-checker for Node-RED applications.

KW - Formal Verification

KW - Internet of Things

KW - Node-RED

KW - Petri nets

UR - https://www.scopus.com/pages/publications/85180807303

U2 - 10.1007/978-3-031-49737-7_7

DO - 10.1007/978-3-031-49737-7_7

M3 - Conference contribution

AN - SCOPUS:85180807303

SN - 9783031497360

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 90

EP - 104

BT - Verification and Evaluation of Computer and Communication Systems - 16th International Conference, VECoS 2023, Proceedings

A2 - Ben Hedia, Belgacem

A2 - Maleh, Yassine

A2 - Krichen, Moez

PB - Springer Science and Business Media Deutschland GmbH

T2 - 16th International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS 2023

Y2 - 18 October 2023 through 20 October 2023

ER -

Garfatta I, Souid NE, Klai K. Towards Formal Verification of Node RED-Based IoT Applications. In Ben Hedia B, Maleh Y, Krichen M, editors, Verification and Evaluation of Computer and Communication Systems - 16th International Conference, VECoS 2023, Proceedings. Springer Science and Business Media Deutschland GmbH. 2024. p. 90-104. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-49737-7_7