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.