The Internet of Things (IoT) is announced to swamp the world. In order to understand the emergent behaviour of connected things, effective support for the modelling of connection and failure probabilities, execution and waiting times, as well as resource consumptions of various kinds is needed. At the heart of IoT are flexible and adaptive communication and interaction patterns between things, meant to enable advanced as well as radically new emerging functionalities. Since these interaction patterns are determined by topological characteristics, they can naturally be modelled by channel-based exogenous coordination primitives. In this paper, we tackle the IoT modelling challenge. Our modelling approach is based on a conservative extension of Reo circuits. On a technical level, we work with a model called Priced Probabilistic Timed Constraint Automaton, which combines existing models of probabilistic and timed aspects, and is equipped with pricing information. The latter enables us to reason about resource consumption, especially important in light of severely limited power, memory and computation budgets in things. The approach is set up in such a way that the original constituent models can be retrieved without changes in syntax and semantics. A small but illustrative IoT case is modelled and evaluated, demonstrating the principal benefits of the proposed approach.

Probabilistic Model-Checking is a standard approach for automatically verifying stochastic systems. However, it becomes expensive or even intractable for classic approaches to verify complex systems. Statistical model-checking was proposed to overcome this limitation. In this paper, we propose a novel statistical model-checking approach which is based on Bayesian point estimation. Together with the Bayesian point estimation and a given conjugate prior distribution, we are able to predict the upper bound of sample size before sampling. We implement our techniques in a tool. Experiential results show that our approach is competitive, even better than other standard approaches in several cases.

Pipe protocol, proposed by Zhao [1] in early 2013, is one application layer protocol and one way to establish the Internet of Things, under which can different kinds of hardware platforms communicate with each other faster and more safely. As an upper layer protocol, Pipe protocol doesn't define details, but during the implementation, probabilistic and nondeterministic behaviors, such as data loss and external choice, are possible to happen. In this paper, we use probabilistic model checker, PRISM, to construct the probabilistic Pipe protocol as Probabilistic Timed Automata (PTAs), then verify some useful time-bounded properties, written in Probabilistic Computation Tree Logic (PCTL), like, “Maximum probability that the pipe is shut down after Source node sends all 5 data packets within 50 μs”. The results show that the data loss probabilities, number of data and deadline should be restricted suitably if we require the maximum probability of the goal reaches some value. Our model is proved to be meaningful and we can give helpful suggestions to improve the implementation of Pipe protocol.