Modeling and verification of the Multi-connection Tactile Internet Protocol

Abstract

Tactile Internet (TI) refers to the transmission of touch and the real-time control of applications like the remote control for teleoperation of machines, drones or vehicles. Traditional TCP and UDP protocols are not suitable for these applications, because they are mainly designed for content delivery or non real-time interactive applications. Some ideas from transport protocols for real-time multimedia like RTP are closer to Tactile Internet; however, they do not satisfy requirements of low latency and high reliability. In this paper, we present the Multi-connection Tactile Internet Protocol (MTIP), a novel transport protocol on top of the Internet Protocol to support the reliability and latency for Internet applications over multi-homed devices connected to several wireless networks. In order to provide that service, MTIP is based on the combination of sequence numbers and timestamps in packets, enhanced with global clocks and context awareness. The paper focuses on building a state machine based model of MTIP to prove the correct behaviour of the protocol using the SPIN tool to verify a number of relevant correctness properties.