Connection models for the Internet-of-Things

doi:10.1007/s11704-018-7395-3

Front. Comput. Sci.

2020, Vol. 14

Issue (3) : 143401 https://doi.org/10.1007/s11704-018-7395-3

RESEARCH ARTICLE

Connection models for the Internet-of-Things

Kangli HE¹, Holger HERMANNS², Hengyang WU¹, Yixiang CHEN¹(

)

¹. MoE Engineering Research Center for Software/Hardware Co-design Technology and Application, East China Normal University, Shanghai 200062, China
². Saarland University, Saarland Informatics Campus, Saarbrücken 66123, Germany

Download: PDF(882 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Corresponding Author(s): Yixiang CHEN

Issue Date: 10 January 2020

Cite this article:

Kangli HE,Holger HERMANNS,Hengyang WU, et al. Connection models for the Internet-of-Things[J]. Front. Comput. Sci., 2020, 14(3): 143401.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-018-7395-3
https://academic.hep.com.cn/fcs/EN/Y2020/V14/I3/143401

1	E Borgia. The Internet of Things vision: key features, applications and open issues. Computer Communications, 2014, 54: 1–31
2	I Lanese, L Bedogni, M D Felice. Internet of Things: a process calculus approach. In: Proceedings of Annual ACM Symposium on Applied Computing. 2013, 1339–1346
3	R Lanotte, M Merro. A semantic theory of the internet of things. Information and Computation, 2018, 259(1): 72–101
4	F Arbab. Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science, 2004, 14(3): 329–366
5	S Meng, F Arbab. On resource-sensitive timed component connectors. In: Proceedings of International Conference on Formal Methods for Open Object-Based Distributed Systems. 2007, 301–316
6	F Arbab, T Chothia, S Meng, Y J Moon. Component connectors with QoS guarantees. In: Proceedings of International Conference on Coordination Models and Languages. 2007, 286–304
7	C Baier, M Sirjani, F Arbab, J Rutten. Modeling component connectors in Reo by constraint automata. Science of Computer Programming, 2006, 61(2): 75–113
8	S S T Q Jongmans, F Arbab. Overview of thirty semantic formalisms for Reo. Scientific Annals of Computer Science, 2012, 22(1): 201–251
9	F Arbab, C Baier, F de Boer, J Rutten. Models and temporal logical specifications for timed component connectors. Software and System Modeling, 2007, 6(1): 59–82
10	C Baier. Probabilistic models for Reo connector circuits. Journal of Universal Computer Science, 2005, 11(10): 1718–1748
11	A Aziz, V Singhal, F Balarin. It usually works: the temporal logic of stochastic systems. In: Proceedings of International Conference on Computer Aided Verification. 1995, 155–165
12	K He, H Hermanns, Y Chen. Models of connected things: on priced probabilistic timed Reo. In: Proceedings of IEEE Annual Computer Software and Applications Conference. 2017, 234–243
13	F Arbab, J J M M Rutten. A coinductive calculus of component connectors. In: Proceedings of International Workshop on Recent Trends in Algebraic Development Techniques. 2002, 34–55
14	R Alur, D L Dill. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183–235
15	T A Henzinger, X Nicollin, J Sifakis, S Yovine. Symbolic model checking for real-time systems. Information and Computation, 1994, 111(2): 193–244
16	R Segala, N A Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 1995, 2(2): 250–273
17	A Turrini, H Hermanns. Cost preserving bisimulations for probabilistic automata. Logical Methods in Computer Science, 2014, 10(4): 1–58
18	R Segala. Modelling and verification of randomized distributed real time systems. PhD Thesis, Cambridge: Massachusetts Institute of Technology, 1995
19	R V Glabbeek, S A Smolka, B Steffen, C M N Tofts. Reactive, generative, and stratified models of probabilistic processes. In: Proceedings of Annual Symposium on Logic in Computer Science. 1990, 130–141
20	R V Glabbeek, S A Smolka, B Steffen. Reactive, generative and stratified models of probabilistic processes. Information and Computation, 1995, 121(1): 59–80
21	P R D’ Argenio, H Hermanns, J P Katoen. On generative parallel composition. Electronic Notes in Theoretical Computer Science, 1999, 22: 30–54
22	J C M Baeten, J A Bergstra, S A Smolka. Axiomatizing probabilistic processes: ACP with generative probabilities. Information and Computation, 1995, 121(2): 234–255
23	M Z Kwiatkowska, G Norman, D Parker, J Sproston. Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design, 2006, 29(1): 33–78
24	P R Halmos. Measure Theory. Berlin: Springer-Verlag, 1950
25	E M Clarke, E A Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Proceedings of Workshop on Logics of Programs. 1981, 52–71
26	G Norman, D Parker, J Sproston. Model checking for probabilistic timed automata. Formal Methods in System Design, 2013, 43(2): 164–190
27	C Baier, B R Haverkort, H Hermanns, J P Katoen. Performance evaluation and model checking join forces. Communications of the ACM, 2010, 53(9): 76–85
28	A Bianco, L D Alfaro. 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	E Asarin, P Caspi, O Maler. Timed regular expressions. Journal of the ACM, 2002, 49(2): 172–206
30	H Hansson, B Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994, 6(5): 512–535
31	A Bianco, L D Alfaro. 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	L Li, Z Jin, G Li, L Zheng, Q Wei. 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	G Li, Q Wei, X Li, Z Jin, Y Xu, L Zheng. Environment based modeling approach for services in the internet of things. Scientia Sinica, 2013, 43(10): 1198–1218
34	B Martinez, M Montón, I Vilajosana, J D Prades. The power of models: modeling power consumption for IoT devices. IEEE Sensors Journal, 2015, 15(10): 5777–5789
35	B Costa, P F Pires, F C Delicato, W Li, A Y Zomaya. 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	E A Lee. Cyber physical systems: design challenges. In: Proceedings of IEEE International Symposium on Object-Oriented Real-Time Distributed Computing. 2008, 363–369
37	E Palomar, X Chen, Z Liu, S Maharjan, J P Bowen. Componentbased modelling for scalable smart city systems interoperability: a case study on integrating energy demand response systems. Sensors, 2016, 16(11): 1810
38	C Baier, V Wolf. Stochastic reasoning about channel-based component connectors. In: Proceedings of International Conference on Coordination Models and Languages. 2006, 1–15
39	Y J Moon, A Silva, C Krause, F Arbab. 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	N Oliveira, A Silva, L A Barbosa. IMCReo: interactive Markov chains for stochastic Reo. Journal of Internet Services and Information Security, 2015, 5(1): 3–28
41	A Pnueli. The temporal logic of programs. In: Proceedings of Annual Symposium on Foundations of Computer Science. 1977, 46–57
42	H C Bohnenkamp, P R D’ Argenio, H Hermanns, J P Katoen. Modest: a compositional modeling formalism for hard and softly timed systems. IEEE Transactions on Software Engineering, 2006, 32(10): 812–830
43	E M Hahn, A Hartmanns, H Hermanns, J P Katoen. A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods in System Design, 2013, 43(2): 191–232

[1]

Article highlights

Download

[1]	Zhiyong YU, Xiangping ZHENG, Fangwan HUANG, Wenzhong GUO, Lin SUN, Zhiwen YU. A framework based on sparse representation model for time series prediction in smart city[J]. Front. Comput. Sci., 2021, 15(1): 151305-.
[2]	Xingxing HAO, Jing LIU, Yutong ZHANG, Gustaph SANGA. Mathematical model and simulated annealing algorithm for Chinese high school timetabling problems under the new curriculum innovation[J]. Front. Comput. Sci., 2021, 15(1): 151309-.
[3]	Gan HUANG, Hee Yong YOUN. Proactive eviction of flow entry for SDN based on hidden Markov model[J]. Front. Comput. Sci., 2020, 14(4): 144502-.
[4]	Daian YUE, Vania JOLOBOFF, Frédéric MALLET. TRAP: trace runtime analysis of properties[J]. Front. Comput. Sci., 2020, 14(3): 143201-.
[5]	Ebuka IBEKE, Chenghua LIN, Adam WYNER, Mohamad Hardyman BARAWI. A unified latent variable model for contrastive opinion mining[J]. Front. Comput. Sci., 2020, 14(2): 404-416.
[6]	Chao CHEN, Liping GAO, Xuefeng XIE, Zhu WANG. Enjoy the most beautiful scene now: a memetic algorithm to solve two-fold time-dependent arc orienteering problem[J]. Front. Comput. Sci., 2020, 14(2): 364-377.
[7]	Huiping LIU, Cheqing JIN, Aoying ZHOU. Popular route planning with travel cost estimation from trajectories[J]. Front. Comput. Sci., 2020, 14(1): 191-207.
[8]	Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[9]	Yi ZHOU, Qichuan GENG, Zhong ZHOU, Wei WU. Automatic façade recovery from single nighttime image[J]. Front. Comput. Sci., 2020, 14(1): 95-104.
[10]	Gaochang WU, Yipeng LI, Yuanhao HUANG, Yebin LIU. Joint view synthesis and disparity refinement for stereo matching[J]. Front. Comput. Sci., 2019, 13(6): 1337-1352.
[11]	Ningnan ZHOU, Xiao ZHANG, Shan WANG. Timestamp reassignment: taming transaction abort for serializable snapshot isolation[J]. Front. Comput. Sci., 2019, 13(6): 1282-1295.
[12]	Juan CHEN, Wenhao ZHOU, Yong DONG, Zhiyuan WANG, Chen CUI, Feihao WU, Enqiang ZHOU, Yuhua TANG. Analyzing time-dimension communication characterizations for representative scientific applications on supercomputer systems[J]. Front. Comput. Sci., 2019, 13(6): 1228-1242.
[13]	Wen LIU, Tuqian ZHANG, Yanming SHEN, Peng WANG. Fast correlation coefficient estimation algorithm for HBase-based massive time series data[J]. Front. Comput. Sci., 2019, 13(4): 864-878.
[14]	Kai HU, Zhangbo DUAN, Jiye WANG, Lingchao GAO, Lihong SHANG. Template-based AADL automatic code generation[J]. Front. Comput. Sci., 2019, 13(4): 698-714.
[15]	Thierry GAUTIER, Clément GUY, Alexandre HONORAT, Paul LE GUERNIC, Jean-Pierre TALPIN, Loïc BESNARD. Polychronous automata and their use for formal validation of AADL models[J]. Front. Comput. Sci., 2019, 13(4): 677-697.

Viewed

Full text

Abstract

Cited

Shared

Discussed