The Internet-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 an...The Internet-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 patterns 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.展开更多
基金supported by the National Natural Science Foundation of China(Grant Nos.61370100,61321064 and 61773019)Shanghai Knowledge Service Platform for Trustworthy Internet of Things(ZF1213)+2 种基金Shanghai Municipal Science and Technology Commission Project(1451100400)Defense Industrial Technology Development Program JCKY 2016212B004-2,by the ERC Advanced Grant 695614(POWVER)by the Sino-German Center for Research Project CAP(GZ 1023).
文摘The Internet-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 patterns 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.
