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

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

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). 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. We use temporal logic in the representation of this protocol model to ensure the safety of systems. Administrative routing protocols benefit significantly from this protocol model.

Original languageEnglish
Title of host publicationCyberspace Data and Intelligence, and Cyber-Living, Syndrome, and Health
Subtitle of host publicationInternational 2019 Cyberspace Congress, CyberDI and Cyberlife, Beijing, China, December 16-19, 2019, Proceedings, Part 11
EditorsHuansheng Ning
PublisherSpringer Singapore
Pages149-168
Number of pages20
Edition1st
ISBN (Electronic)9789811519253
ISBN (Print)9789811519246, 9789811519215
DOIs
Publication statusPublished - 6 Dec 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 Singapore
Volume1138
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

Linear Temporal Logic
Temporal logic
Concurrent Systems
Networking
Specification
Specifications
Network protocols
Concurrent
Safety
Cycle
Transactions
Routing protocols
Security systems
Routers
Internet of Things
Mobile Systems
Computer systems
Temporal Logic
Graph in graph theory
Routing Protocol

Cite this

Abdelrahman, R. B., Al-Aqrabi, H., & Hill, R. (2019). An efficient concurrent system networking protocol specification and verification using linear temporal logic. In H. Ning (Ed.), Cyberspace Data and Intelligence, and Cyber-Living, Syndrome, and Health: International 2019 Cyberspace Congress, CyberDI and Cyberlife, Beijing, China, December 16-19, 2019, Proceedings, Part 11 (1st ed., pp. 149-168). (Communications in Computer and Information Science; Vol. 1138). Springer Singapore. https://doi.org/10.1007/978-981-15-1925-3_12
Abdelrahman, Ra-ed Bani ; Al-Aqrabi, Hussain ; Hill, Richard. / An efficient concurrent system networking protocol specification and verification using linear temporal logic. Cyberspace Data and Intelligence, and Cyber-Living, Syndrome, and Health: International 2019 Cyberspace Congress, CyberDI and Cyberlife, Beijing, China, December 16-19, 2019, Proceedings, Part 11. editor / Huansheng Ning. 1st. ed. Springer Singapore, 2019. pp. 149-168 (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 are of principal concern, especially when dealing with concurrent transactions on which mobile systems depend on, such as the emerging Internet of Things (IoT). 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. We use temporal logic in the representation of this protocol model to ensure the safety of systems. Administrative routing protocols benefit significantly from this protocol model.",
keywords = "Concurrent transactions, Conflict graphs, Output schedules, Routing protocol",
author = "Abdelrahman, {Ra-ed Bani} and Hussain Al-Aqrabi and Richard Hill",
year = "2019",
month = "12",
day = "6",
doi = "10.1007/978-981-15-1925-3_12",
language = "English",
isbn = "9789811519246",
series = "Communications in Computer and Information Science",
publisher = "Springer Singapore",
pages = "149--168",
editor = "Huansheng Ning",
booktitle = "Cyberspace Data and Intelligence, and Cyber-Living, Syndrome, and Health",
address = "Singapore",
edition = "1st",

}

Abdelrahman, RB, Al-Aqrabi, H & Hill, R 2019, An efficient concurrent system networking protocol specification and verification using linear temporal logic. in H Ning (ed.), Cyberspace Data and Intelligence, and Cyber-Living, Syndrome, and Health: International 2019 Cyberspace Congress, CyberDI and Cyberlife, Beijing, China, December 16-19, 2019, Proceedings, Part 11. 1st edn, Communications in Computer and Information Science, vol. 1138, Springer Singapore, pp. 149-168, International Conference on Cyberspace Data and Intelligence 2019, Beijing, China, 16/12/19. https://doi.org/10.1007/978-981-15-1925-3_12

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

Cyberspace Data and Intelligence, and Cyber-Living, Syndrome, and Health: International 2019 Cyberspace Congress, CyberDI and Cyberlife, Beijing, China, December 16-19, 2019, Proceedings, Part 11. ed. / Huansheng Ning. 1st. ed. Springer Singapore, 2019. p. 149-168 (Communications in Computer and Information Science; Vol. 1138).

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 - Abdelrahman, Ra-ed Bani

AU - Al-Aqrabi, Hussain

AU - Hill, Richard

PY - 2019/12/6

Y1 - 2019/12/6

N2 - 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). 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. We use temporal logic in the representation of this protocol model to ensure the safety of systems. Administrative routing protocols benefit significantly from this protocol model.

AB - 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). 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. We use temporal logic in the representation of this protocol model to ensure the safety of systems. Administrative routing protocols benefit significantly from this protocol model.

KW - Concurrent transactions

KW - Conflict graphs

KW - Output schedules

KW - Routing protocol

UR - https://www.springerprofessional.de/en/cyberspace-data-and-intelligence-and-cyber-living-syndrome-and-h/17492556?tocPage=1

UR - http://www.scopus.com/inward/record.url?scp=85076922504&partnerID=8YFLogxK

U2 - 10.1007/978-981-15-1925-3_12

DO - 10.1007/978-981-15-1925-3_12

M3 - Conference contribution

SN - 9789811519246

SN - 9789811519215

T3 - Communications in Computer and Information Science

SP - 149

EP - 168

BT - Cyberspace Data and Intelligence, and Cyber-Living, Syndrome, and Health

A2 - Ning, Huansheng

PB - Springer Singapore

ER -

Abdelrahman RB, Al-Aqrabi H, Hill R. An efficient concurrent system networking protocol specification and verification using linear temporal logic. In Ning H, editor, Cyberspace Data and Intelligence, and Cyber-Living, Syndrome, and Health: International 2019 Cyberspace Congress, CyberDI and Cyberlife, Beijing, China, December 16-19, 2019, Proceedings, Part 11. 1st ed. Springer Singapore. 2019. p. 149-168. (Communications in Computer and Information Science). https://doi.org/10.1007/978-981-15-1925-3_12