Connection models for the Internet-of-Things

Abstract

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.

Keywords

IoT / Reo / cost / time / probability / automaton

References

[1] Borgia E. The Internet of Things vision: key features, applications and open issues. Computer Communications, 2014, 54: 1–31

[2] Lanese I, Bedogni L, Felice M D. Internet of Things: a process calculus approach. In: Proceedings of Annual ACM Symposium on Applied Computing. 2013, 1339–1346

[3] Lanotte R, Merro M. A semantic theory of the internet of things. Information and Computation, 2018, 259(1): 72–101

[4] Arbab F. Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science, 2004, 14(3): 329–366

[5] Meng S, Arbab F. On resource-sensitive timed component connectors. In: Proceedings of International Conference on Formal Methods for Open Object-Based Distributed Systems. 2007, 301–316

[6] Arbab F, Chothia T, Meng S, Moon Y J. Component connectors with QoS guarantees. In: Proceedings of International Conference on Coordination Models and Languages. 2007, 286–304

[7] Baier C, Sirjani M, Arbab F, Rutten J. Modeling component connectors in Reo by constraint automata. Science of Computer Programming, 2006, 61(2): 75–113

[8] Jongmans S S T Q, Arbab F. Overview of thirty semantic formalisms for Reo. Scientific Annals of Computer Science, 2012, 22(1): 201–251

[9] Arbab F, Baier C, de Boer F, Rutten J. Models and temporal logical specifications for timed component connectors. Software and System Modeling, 2007, 6(1): 59–82

[10] Baier C. Probabilistic models for Reo connector circuits. Journal of Universal Computer Science, 2005, 11(10): 1718–1748

[11] Aziz A, Singhal V, Balarin F. It usually works: the temporal logic of stochastic systems. In: Proceedings of International Conference on Computer Aided Verification. 1995, 155–165

[12] He K, Hermanns H, Chen Y. Models of connected things: on priced probabilistic timed Reo. In: Proceedings of IEEE Annual Computer Software and Applications Conference. 2017, 234–243

[13] Arbab F, Rutten J J M M. A coinductive calculus of component connectors. In: Proceedings of International Workshop on Recent Trends in Algebraic Development Techniques. 2002, 34–55

[14] Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183–235

[15] Henzinger T A, Nicollin X, Sifakis J, Yovine S. Symbolic model checking for real-time systems. Information and Computation, 1994, 111(2): 193–244

[16] Segala R, Lynch N A. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 1995, 2(2): 250–273

[17] Turrini A, Hermanns H. Cost preserving bisimulations for probabilistic automata. Logical Methods in Computer Science, 2014, 10(4): 1–58

[18] Segala R. Modelling and verification of randomized distributed real time systems. PhD Thesis, Cambridge: Massachusetts Institute of Technology, 1995

[19] Glabbeek R V, Smolka S A, Steffen B, Tofts C M N. Reactive, generative, and stratified models of probabilistic processes. In: Proceedings of Annual Symposium on Logic in Computer Science. 1990, 130–141

[20] Glabbeek R V, Smolka S A, Steffen B. Reactive, generative and stratified models of probabilistic processes. Information and Computation, 1995, 121(1): 59–80

[21] D’ Argenio P R, Hermanns H, Katoen J P. On generative parallel composition. Electronic Notes in Theoretical Computer Science, 1999, 22: 30–54

[22] Baeten J C M, Bergstra J A, Smolka S A. Axiomatizing probabilistic processes: ACP with generative probabilities. Information and Computation, 1995, 121(2): 234–255

[23] Kwiatkowska M Z, Norman G, Parker D, Sproston J. Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design, 2006, 29(1): 33–78

[24] Halmos P R. Measure Theory. Berlin: Springer-Verlag, 1950

[25] Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Proceedings of Workshop on Logics of Programs. 1981, 52–71

[26] Norman G, Parker D, Sproston J. Model checking for probabilistic timed automata. Formal Methods in System Design, 2013, 43(2): 164–190

[27] Baier C, Haverkort B R, Hermanns H, Katoen J P. Performance evaluation and model checking join forces. Communications of the ACM, 2010, 53(9): 76–85

[28] Bianco A, Alfaro L D. Model checking of probabilistic and nondeterministic systems. In: Proceedings of International Conference on Foundations of Software Technology and Theoretical Computer Science. 1995, 499–513

[29] Asarin E, Caspi P, Maler O. Timed regular expressions. Journal of the ACM, 2002, 49(2): 172–206

[30] Hansson H, Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994, 6(5): 512–535

[31] Bianco A, Alfaro L D. Model checking of probabalistic and nondeterministic systems. In: Proceedings of International Conference on Foundations of Software Technology and Theoretical Computer Science. 1995, 499–513

[32] Li L, Jin Z, Li G, Zheng L, Wei Q. Modeling and analyzing the reliability and cost of service composition in the IoT: a probabilistic approach. In: Proceedings of International Conference on Web Services. 2012, 584–591

[33] Li G, Wei Q, Li X, Jin Z, Xu Y, Zheng L. Environment based modeling approach for services in the internet of things. Scientia Sinica, 2013, 43(10): 1198–1218

[34] Martinez B, Montón M, Vilajosana I, Prades J D. The power of models: modeling power consumption for IoT devices. IEEE Sensors Journal, 2015, 15(10): 5777–5789

[35] Costa B, Pires P F, Delicato F C, Li W, Zomaya A Y. Design and analysis of iot applications: a model-driven approach. In: Proceedings of the 14th International Conference on Dependable, Autonomic and Secure Computing, the 14th International Conference on Pervasive Intelligence and Computing, the 2nd International Conference on Big Data Intelligence and Computing and Cyber Science and Technology Congress. 2016, 392–399

[36] Lee E A. Cyber physical systems: design challenges. In: Proceedings of IEEE International Symposium on Object-Oriented Real-Time Distributed Computing. 2008, 363–369

[37] Palomar E, Chen X, Liu Z, Maharjan S, Bowen J P. Componentbased modelling for scalable smart city systems interoperability: a case study on integrating energy demand response systems. Sensors, 2016, 16(11): 1810

[38] Baier C, Wolf V. Stochastic reasoning about channel-based component connectors. In: Proceedings of International Conference on Coordination Models and Languages. 2006, 1–15

[39] Moon Y J, Silva A, Krause C, Arbab F. A compositional semantics for stochastic Reo connectors. In: Proceedings of International Workshop on the Foundations of Coordination Languages and Software Architectures. 2010, 93–107

[40] Oliveira N, Silva A, Barbosa L A. IMCReo: interactive Markov chains for stochastic Reo. Journal of Internet Services and Information Security, 2015, 5(1): 3–28

[41] Pnueli A. The temporal logic of programs. In: Proceedings of Annual Symposium on Foundations of Computer Science. 1977, 46–57

[42] Bohnenkamp H C, D’ Argenio P R, Hermanns H, Katoen J P. Modest: a compositional modeling formalism for hard and softly timed systems. IEEE Transactions on Software Engineering, 2006, 32(10): 812–830

[43] Hahn E M, Hartmanns A, Hermanns H, Katoen J P. A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods in System Design, 2013, 43(2): 191–232

RIGHTS & PERMISSIONS

2019 Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature