IoTC2: A formal method approach for detecting conflicts in large scale IoT systems

Abdullah Al Farooq; Ehab Al-Shaer; Thomas Moyer; Krishna Kant

IoTC²: A formal method approach for detecting conflicts in large scale IoT systems

Abdullah Al Farooq, Ehab Al-Shaer, Thomas Moyer, Krishna Kant

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

31 Scopus citations

Abstract

Internet of Things (IoT) has become a common paradigm for different domains such as health care, transportation infrastructure, smart homes, smart shopping, and e-commerce. With its interoperable functionality, it is now possible to connect all domains of IoT together to provide comprehensive services to the users. Because numerous IoT devices can connect and communicate at the same time, there can be events that trigger conflicting actions for an actuator or an environmental feature. This paper provides a formal method approach, IoT Confict Checker (IoTC²), to ensure safety of controller and actuators' behavior with respect to conflicts. Any policy violation results in detection of the conflicts. We define the safety policies for controller, actions, and triggering events and implement them in Prolog to prove the logical completeness and soundness. In addition to that, we have implemented the detection policies in Matlab Simulink Environment with its built-in Model Verification blocks. We created a smart home environment in Simulink and showed how the conflicts affect actions and corresponding features. The scalability, efficiency, and accuracy of our method are tested in this simulated environment.

Original language	English
Title of host publication	2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	442-447
Number of pages	6
ISBN (Electronic)	9783903176157
State	Published - 16 May 2019
Externally published	Yes
Event	2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019 - Arlington, United States Duration: 8 Apr 2019 → 12 Apr 2019

Publication series

Name	2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019

Conference

Conference	2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019
Country/Territory	United States
City	Arlington
Period	8/04/19 → 12/04/19

Bibliographical note

Publisher Copyright:
© 2019 IFIP.

Keywords

Conflicts
Formal Method
Internet of Things(IoT)
Policies
Safety
Security
Simulation

ASJC Scopus subject areas

Information Systems and Management
Management Science and Operations Research
Information Systems
Computer Networks and Communications

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Cite this

Al Farooq, A., Al-Shaer, E., Moyer, T., & Kant, K. (2019). IoTC²: A formal method approach for detecting conflicts in large scale IoT systems. In 2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019 (pp. 442-447). Article 8717844 (2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019). Institute of Electrical and Electronics Engineers Inc..

Al Farooq, Abdullah ; Al-Shaer, Ehab ; Moyer, Thomas et al. / IoTC² : A formal method approach for detecting conflicts in large scale IoT systems. 2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019. Institute of Electrical and Electronics Engineers Inc., 2019. pp. 442-447 (2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019).

@inproceedings{96301836dc334afe8ced468fde48707b,

title = "IoTC2: A formal method approach for detecting conflicts in large scale IoT systems",

abstract = "Internet of Things (IoT) has become a common paradigm for different domains such as health care, transportation infrastructure, smart homes, smart shopping, and e-commerce. With its interoperable functionality, it is now possible to connect all domains of IoT together to provide comprehensive services to the users. Because numerous IoT devices can connect and communicate at the same time, there can be events that trigger conflicting actions for an actuator or an environmental feature. This paper provides a formal method approach, IoT Confict Checker (IoTC2), to ensure safety of controller and actuators' behavior with respect to conflicts. Any policy violation results in detection of the conflicts. We define the safety policies for controller, actions, and triggering events and implement them in Prolog to prove the logical completeness and soundness. In addition to that, we have implemented the detection policies in Matlab Simulink Environment with its built-in Model Verification blocks. We created a smart home environment in Simulink and showed how the conflicts affect actions and corresponding features. The scalability, efficiency, and accuracy of our method are tested in this simulated environment.",

keywords = "Conflicts, Formal Method, Internet of Things(IoT), Policies, Safety, Security, Simulation",

author = "\{Al Farooq\}, Abdullah and Ehab Al-Shaer and Thomas Moyer and Krishna Kant",

note = "Publisher Copyright: {\textcopyright} 2019 IFIP.; 2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019 ; Conference date: 08-04-2019 Through 12-04-2019",

year = "2019",

month = may,

day = "16",

language = "English",

series = "2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "442--447",

booktitle = "2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019",

address = "United States",

}

Al Farooq, A, Al-Shaer, E, Moyer, T & Kant, K 2019, IoTC²: A formal method approach for detecting conflicts in large scale IoT systems. in 2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019., 8717844, 2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019, Institute of Electrical and Electronics Engineers Inc., pp. 442-447, 2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019, Arlington, United States, 8/04/19.

IoTC²: A formal method approach for detecting conflicts in large scale IoT systems. / Al Farooq, Abdullah; Al-Shaer, Ehab; Moyer, Thomas et al.
2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019. Institute of Electrical and Electronics Engineers Inc., 2019. p. 442-447 8717844 (2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019).

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

TY - GEN

T1 - IoTC2

T2 - 2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019

AU - Al Farooq, Abdullah

AU - Al-Shaer, Ehab

AU - Moyer, Thomas

AU - Kant, Krishna

PY - 2019/5/16

Y1 - 2019/5/16

N2 - Internet of Things (IoT) has become a common paradigm for different domains such as health care, transportation infrastructure, smart homes, smart shopping, and e-commerce. With its interoperable functionality, it is now possible to connect all domains of IoT together to provide comprehensive services to the users. Because numerous IoT devices can connect and communicate at the same time, there can be events that trigger conflicting actions for an actuator or an environmental feature. This paper provides a formal method approach, IoT Confict Checker (IoTC2), to ensure safety of controller and actuators' behavior with respect to conflicts. Any policy violation results in detection of the conflicts. We define the safety policies for controller, actions, and triggering events and implement them in Prolog to prove the logical completeness and soundness. In addition to that, we have implemented the detection policies in Matlab Simulink Environment with its built-in Model Verification blocks. We created a smart home environment in Simulink and showed how the conflicts affect actions and corresponding features. The scalability, efficiency, and accuracy of our method are tested in this simulated environment.

AB - Internet of Things (IoT) has become a common paradigm for different domains such as health care, transportation infrastructure, smart homes, smart shopping, and e-commerce. With its interoperable functionality, it is now possible to connect all domains of IoT together to provide comprehensive services to the users. Because numerous IoT devices can connect and communicate at the same time, there can be events that trigger conflicting actions for an actuator or an environmental feature. This paper provides a formal method approach, IoT Confict Checker (IoTC2), to ensure safety of controller and actuators' behavior with respect to conflicts. Any policy violation results in detection of the conflicts. We define the safety policies for controller, actions, and triggering events and implement them in Prolog to prove the logical completeness and soundness. In addition to that, we have implemented the detection policies in Matlab Simulink Environment with its built-in Model Verification blocks. We created a smart home environment in Simulink and showed how the conflicts affect actions and corresponding features. The scalability, efficiency, and accuracy of our method are tested in this simulated environment.

KW - Conflicts

KW - Formal Method

KW - Internet of Things(IoT)

KW - Policies

KW - Safety

KW - Security

KW - Simulation

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

M3 - Conference contribution

AN - SCOPUS:85067040255

T3 - 2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019

SP - 442

EP - 447

BT - 2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019

PB - Institute of Electrical and Electronics Engineers Inc.

Y2 - 8 April 2019 through 12 April 2019

ER -

Al Farooq A, Al-Shaer E, Moyer T, Kant K. IoTC²: A formal method approach for detecting conflicts in large scale IoT systems. In 2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019. Institute of Electrical and Electronics Engineers Inc. 2019. p. 442-447. 8717844. (2019 IFIP/IEEE Symposium on Integrated Network and Service Management, IM 2019).