An efficient concurrent system networking protocol specification and verification using linear temporal logic

Richard Hill, Ra-ed Bani Abdelrahman, Hussain Al-Aqrabi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In critical computer-based systems, safety and reliability are
of principal concern, especially when dealing with concurrent transactions on which mobile systems depend on, such as the emerging Internet of Things (IoT). In this paper, we present a protocol to ensure safety and reliability of systems where concurrent modification of data on routers in a network is possible, by detecting cycles in the conflict graph and ensuring the system is free of any cycle in an effective manner. The existence of a cycle in a conflict graph means that the schedule of such concurrent transactions cannot be serialized (i.e., not correct). We use temporal logic in the representation of this protocol model since it is one of the more effective and distinctive methods used to ensure the safety of systems. The routers are accessed concurrently where a gap is allowed.
Administrative routing protocols benefit significantly from this protocol model.
Original languageEnglish
Title of host publicationInternational Conference on Cyberspace Data and Intelligence 2019 (CyberDI2019)
PublisherSpringer Verlag
Number of pages20
Publication statusAccepted/In press - 14 Oct 2019
EventInternational Conference on Cyberspace Data and Intelligence 2019 - Beijing, China
Duration: 16 Dec 201918 Dec 2019
http://www.cybermatics.org/CyberCon/CyberDI2019/

Publication series

NameCommunications in Computer and Information Science
PublisherSpringer Verlag
ISSN (Electronic)1865-0929

Conference

ConferenceInternational Conference on Cyberspace Data and Intelligence 2019
Abbreviated titleCyberDI 2019
CountryChina
CityBeijing
Period16/12/1918/12/19
Internet address

Fingerprint

Temporal logic
Specifications
Routers
Network protocols
Routing protocols
Security systems

Cite this

Hill, R., Abdelrahman, R. B., & Al-Aqrabi, H. (Accepted/In press). An efficient concurrent system networking protocol specification and verification using linear temporal logic. In International Conference on Cyberspace Data and Intelligence 2019 (CyberDI2019) (Communications in Computer and Information Science). Springer Verlag.
Hill, Richard ; Abdelrahman, Ra-ed Bani ; Al-Aqrabi, Hussain. / An efficient concurrent system networking protocol specification and verification using linear temporal logic. International Conference on Cyberspace Data and Intelligence 2019 (CyberDI2019). Springer Verlag, 2019. (Communications in Computer and Information Science).
@inproceedings{86f42e2fa25a439a807a912d323f0302,
title = "An efficient concurrent system networking protocol specification and verification using linear temporal logic",
abstract = "In critical computer-based systems, safety and reliability areof principal concern, especially when dealing with concurrent transactions on which mobile systems depend on, such as the emerging Internet of Things (IoT). In this paper, we present a protocol to ensure safety and reliability of systems where concurrent modification of data on routers in a network is possible, by detecting cycles in the conflict graph and ensuring the system is free of any cycle in an effective manner. The existence of a cycle in a conflict graph means that the schedule of such concurrent transactions cannot be serialized (i.e., not correct). We use temporal logic in the representation of this protocol model since it is one of the more effective and distinctive methods used to ensure the safety of systems. The routers are accessed concurrently where a gap is allowed.Administrative routing protocols benefit significantly from this protocol model.",
keywords = "linear temporal logic, Computer Networks, protocol, verification",
author = "Richard Hill and Abdelrahman, {Ra-ed Bani} and Hussain Al-Aqrabi",
year = "2019",
month = "10",
day = "14",
language = "English",
series = "Communications in Computer and Information Science",
publisher = "Springer Verlag",
booktitle = "International Conference on Cyberspace Data and Intelligence 2019 (CyberDI2019)",

}

Hill, R, Abdelrahman, RB & Al-Aqrabi, H 2019, An efficient concurrent system networking protocol specification and verification using linear temporal logic. in International Conference on Cyberspace Data and Intelligence 2019 (CyberDI2019). Communications in Computer and Information Science, Springer Verlag, International Conference on Cyberspace Data and Intelligence 2019, Beijing, China, 16/12/19.

An efficient concurrent system networking protocol specification and verification using linear temporal logic. / Hill, Richard; Abdelrahman, Ra-ed Bani; Al-Aqrabi, Hussain.

International Conference on Cyberspace Data and Intelligence 2019 (CyberDI2019). Springer Verlag, 2019. (Communications in Computer and Information Science).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - An efficient concurrent system networking protocol specification and verification using linear temporal logic

AU - Hill, Richard

AU - Abdelrahman, Ra-ed Bani

AU - Al-Aqrabi, Hussain

PY - 2019/10/14

Y1 - 2019/10/14

N2 - In critical computer-based systems, safety and reliability areof principal concern, especially when dealing with concurrent transactions on which mobile systems depend on, such as the emerging Internet of Things (IoT). In this paper, we present a protocol to ensure safety and reliability of systems where concurrent modification of data on routers in a network is possible, by detecting cycles in the conflict graph and ensuring the system is free of any cycle in an effective manner. The existence of a cycle in a conflict graph means that the schedule of such concurrent transactions cannot be serialized (i.e., not correct). We use temporal logic in the representation of this protocol model since it is one of the more effective and distinctive methods used to ensure the safety of systems. The routers are accessed concurrently where a gap is allowed.Administrative routing protocols benefit significantly from this protocol model.

AB - In critical computer-based systems, safety and reliability areof principal concern, especially when dealing with concurrent transactions on which mobile systems depend on, such as the emerging Internet of Things (IoT). In this paper, we present a protocol to ensure safety and reliability of systems where concurrent modification of data on routers in a network is possible, by detecting cycles in the conflict graph and ensuring the system is free of any cycle in an effective manner. The existence of a cycle in a conflict graph means that the schedule of such concurrent transactions cannot be serialized (i.e., not correct). We use temporal logic in the representation of this protocol model since it is one of the more effective and distinctive methods used to ensure the safety of systems. The routers are accessed concurrently where a gap is allowed.Administrative routing protocols benefit significantly from this protocol model.

KW - linear temporal logic

KW - Computer Networks

KW - protocol

KW - verification

UR - http://www.cybermatics.org/CyberCon/CyberDI2019/

M3 - Conference contribution

T3 - Communications in Computer and Information Science

BT - International Conference on Cyberspace Data and Intelligence 2019 (CyberDI2019)

PB - Springer Verlag

ER -

Hill R, Abdelrahman RB, Al-Aqrabi H. An efficient concurrent system networking protocol specification and verification using linear temporal logic. In International Conference on Cyberspace Data and Intelligence 2019 (CyberDI2019). Springer Verlag. 2019. (Communications in Computer and Information Science).