Top

Published in:

2019 | OriginalPaper | Chapter

An Efficient Concurrent System Networking Protocol Specification and Verification Using Linear Temporal Logic

Authors : Ra’ed Bani Abdelrahman, Hussain Al-Aqrabi, Richard Hill

Published in: Cyberspace Data and Intelligence, and Cyber-Living, Syndrome, and Health

Publisher: Springer Singapore

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Consensus Performance of Traffic Management System for Cognitive Radio Network: An Agent Control Approach

next chapter Performance Evaluation of Multiparty Authentication in 5G IIoT Environments

Abadi, M., Manna, Z.: Temporal logic programming. J. Symb. Comput. 8(3), 277–295 (1989)MathSciNetMATHCrossRef

Al-Aqrabi, H., Hill, R.: Dynamic multiparty authentication of data analytics services within cloud environments. In: 2018 IEEE 20th International Conference on HPCC, pp. 742–749. IEEE (2018)

Al Aqrabi, H., Liu, L., Hill, R., Antonopoulos, N.: A multi-layer hierarchical inter-cloud connectivity model for sequential packet inspection of tenant sessions accessing BI as a service. In: IEEE International Conference on HPCC, pp. 498–505. IEEE (2014)

Alshorman, R., Fawareh, H.: Reducing conflict graph of multi-step transactions accessing ordered data with gaps. Math. Comput. Sci. 40(1), 1–8 (2013)MathSciNetMATH

Alshorman, R., Hussak, W.: Multi-step transactions specification and verification in a mobile database community. In: 2008 3rd International Conference on Information and Communication Technologies: From Theory to Applications, ICTTA 2008, pp. 1–6. IEEE (2008)

Alshorman, R., Hussak, W.: A serializability condition for multi-step transactions accessing ordered data. Int. J. Comput. Sci. 4, 13–20 (2009)

Alshorman, R., Hussak, W.: Specifying a timestamp-based protocol for multi-step transactions using LTL. World Acad. Sci. Eng. Technol. Int. J. Comput. Electr. Autom. Control Inf. Eng. 4(11), 1716–1723 (2010)

Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH

Bernstein, P.A., Hadzilacos, V., Goodman, N.: Concurrency Control and Recovery in Database Systems. Addison-Wesley Longman Publishing Co. Inc., Boston (1987)

10.

Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2(4), 410–425 (2000)MATHCrossRef

11.

Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)MATH

12.

Hussak, W.: Serializable histories in quantified propositional temporal logic. Int. J. Comput. Math. 81(10), 1203–1211 (2004)MathSciNetMATHCrossRef

13.

Hussak, W.: Specifying strict serializability of iterated transactions in propositional temporal logic. Int. J. Comput. Sci. 2(2), 150–156 (2007)

14.

Hussak, W.: The serializability problem for a temporal logic of transaction queries. J. Appl. Non-Class. Log. 18(1), 67–78 (2008)MathSciNetMATHCrossRef

15.

Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE 3(2), 125–143 (1977)MathSciNetMATHCrossRef

16.

Lamport, L.: What good is temporal logic? IFIP Congress. 83, 657–668 (1983)

17.

Papadimitriou, C.: The Theory of Database Concurrency Control. Computer Science Press, Rockville (1986)MATH

18.

Peled, D., Pnueli, A.: Proving partial order properties. Theor. Comput. Sci. 126(2), 143–182 (1994)MathSciNetMATHCrossRef

19.

Pnueli, A.: Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Current Trends in Concurrency. LNCS, vol. 224, pp. 510–584. Springer, Heidelberg (1986). https://doi.org/10.1007/BFb0027047CrossRef

20.

Elmasri, R., Navathe, S.: Fundamentals of Database Systems, 4th edn. Addison-Wesley, Boston (2004)MATH

21.

Sistla, A.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6(5), 495–511 (1994)MATHCrossRef

22.

Sommerville, I.: Software Engineering. Addison-Wesley, Boston (2010)MATH

23.

Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification, 1st edn. Springer, New York (1992). https://doi.org/10.1007/978-1-4612-0931-7MATHCrossRef

Title: An Efficient Concurrent System Networking Protocol Specification and Verification Using Linear Temporal Logic
Authors: Ra’ed Bani Abdelrahman
Hussain Al-Aqrabi
Richard Hill
Publisher: Springer Singapore
Book: Cyberspace Data and Intelligence, and Cyber-Living, Syndrome, and Health
Print ISBN: 978-981-15-1924-6

Electronic ISBN: 978-981-15-1925-3

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-981-15-1925-3_12

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner