论文部分内容阅读
The Intet-of-Things (IoT) is expected to swamp the world.In order to study and understand the emergent behaviour of connected things,effective support for their modelling is needed.At the heart of IoT are flexible and adaptive connection patts between things,which can naturally be modelled by channel-based coordination primitives,and characteristics of connection failure probabilities,execution and waiting times,as well as resource consumption.The latter is especially important in light of severely limited power and computation budgets inside the things.In this paper,we tackle the IoT modelling challenge,based on a conservative extension of channel-based Reo circuits.We introduce a model called priced probabilistic timed constraint automaton,which combines models of probabilistic and timed aspects,and integrates pricing information.An expressive logic called priced probabilistic timed scheduled data stream logic is presented,so as to enable the specification and verification of properties,which characterize data-flow streams and prices.A small but illustrative IoT case demonstrates the principal benefits of the proposed approach.