IoT in the e-Healthcare domain has recently seen much interest. The IoT applications in this domain involve extensive interactions between many components within open environments, making verifying these applications a significant challenge. This paper introduces a new framework for modelling and verifying IoT applications in the healthcare domain using a practical system verification technique called multi-valued model checking. We focus on applications that involve interactions based on trust protocols under inconsistency. Specifically, we introduce a new logic of trust called (4v-TCTL) to reason about the inconsistency between designers over IoT systems. We use a Smart Glucose Monitoring System as a case study. We model our system and assign six trust properties to be checked against this system. We introduce a new reduction algorithm for reducing our four-valued model checking problem to the two-valued version to reuse an existing model checker called MCMASt. We verified our system using our approach and reported the experimental results.

Multicopy routing strategies have been considered the most applicable approaches to achieve message delivery in Delay Tolerant Networks (DTNs). Epidemic routing and two-hop forwarding routing are two well-reported approaches for delay tolerant networks routing which allow multiple message replicas to be launched in order to increase message delivery ratio and/or reduce message delivery delay. This advantage, nonetheless, is at the expense of additional buffer space and bandwidth overhead. Thus, to achieve efficient utilization of network resources, it is important to come up with an effective message scheduling strategy to determine which messages should be forwarded and which should be dropped in case of buffer is full. This paper investigates a new message scheduling framework for epidemic and two-hop forwarding routing in DTNs, such that the forwarding/dropping decision can be made at a node during each contact for either optimal message delivery ratio or message delivery delay. Extensive simulation results show that the proposed message scheduling framework can achieve better performance than its counterparts.

This paper introduces a novel multicopy routing protocol, called Self-Adaptive Utility-based Routing Protocol (SAURP), for Delay Tolerant Networks (DTNs) that are possibly composed of a vast number of devices in miniature such as smart phones of heterogeneous capacities in terms of energy resources and buffer spaces. SAURP is characterized by the ability of identifying potential opportunities for forwarding messages to their destinations via a novel utility function-based mechanism, in which a suite of environment parameters, such as wireless channel condition, nodal buffer occupancy, and encounter statistics, are jointly considered. Thus, SAURP can reroute messages around nodes experiencing high-buffer occupancy, wireless interference, and/or congestion, while taking a considerably small number of transmissions. The developed utility function in SAURP is proved to be able to achieve optimal performance, which is further analyzed via a stochastic modeling approach. Extensive simulations are conducted to verify the developed analytical model and compare the proposed SAURP with a number of recently reported encounter-based routing approaches in terms of delivery ratio, delivery delay, and the number of transmissions required for each message delivery. The simulation results show that SAURP outperforms all the counterpart multicopy encounter-based routing protocols considered in the study.

This paper introduces a novel routing protocol in Delay Tolerant Networks (DTNs), aiming to solve the online distributed routing problem. By manipulating a collaborative reinforcement learning technique, a group of nodes can cooperate with each other and make a forwarding decision for the stored messages based on a cost function at each contact with another node. The proposed protocol is characterized by not only considering the contact time statistics under a novel contact model, but also looks into the feedback on user behavior and network conditions, such as congestion and buffer occupancy sampled during each previous contact with any other node. Therefore, the proposed protocol can achieve high efficiency via an adaptive and intelligent routing mechanism according to network conditions. Extensive simulation is conducted to verify the proposed protocol, where a comparison is made with a number of existing encounter-based routing protocols in term of the number of transmissions of each message, message delivery delay, and delivery ratio. The results of the simulation demonstrate the effectiveness of the proposed technique.

This paper introduces a multi-copy routing protocol, called Self Adaptive Routing Protocol (SARP), for intermittently connected mobile networks. SARP aims to exploring the possibility of taking nodes as carriers of messages to be delivered among network partitions. The choice of the best carrier for a message is made according to the prediction based on the history of nodal encounters. The paper will argue that the movement of the nodes and their possible future collocation with the recipient of the messages can be used to make intelligent message forwarding decisions. The proposed protocol has been implemented and compared to a number of existing encounter-based routing approaches, where a near-realistic mobility model is used for testing. The performance of the proposed technique is evaluated in terms of delivery delay and the number of transmissions performed. The results of the simulation show that the proposed technique outperforms all existing multi-copy encounter-based routing protocols. Index terms: DTN, multi-copy routing.