×

zbMATH — the first resource for mathematics

A semantic theory of the Internet of things. (English) Zbl 1388.68013
Summary: We propose a process calculus for modelling and reasoning on systems in the Internet of Things paradigm. Our systems interact both with the physical environment, via sensors and actuators, and with smart devices, via short-range and Internet channels. The calculus is equipped with a standard notion of labelled bisimilarity which is proved to be a coinductive characterisation of a well-known contextual equivalence. We use our semantic proof-methods to prove run-time properties of a non-trivial case study as well as system equalities.

MSC:
68M11 Internet topics
68Q55 Semantics in the theory of computing
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
Esterel; Linda; SCEL
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Lanotte, R.; Merro, M., A semantic theory of the Internet of things (extended abstract), (COORDINATION, Lect. Notes Comput. Sci., vol. 9686, (2016), Springer), 157-174
[2] Gubbi, J.; Buyya, R.; Marusic, S.; Palaniswami, M., Internet of things (iot): a vision, architectural elements, and future directions, Future Gener. Comput. Syst., 29, 7, 1645-1660, (2013)
[3] Atzori, L.; Iera, A.; Morabito, G., The Internet of things: a survey, Comput. Netw., 54, 15, 2787-2805, (2010) · Zbl 1208.68071
[4] Miorandi, D.; Sicari, S.; De Pellegrini, F.; Chlamtac, I., Internet of things: vision, applications and research challenges, Ad Hoc Netw., 10, 7, 1497-1516, (2012)
[5] Roussos, G.; Kostakos, V., RFID in pervasive computing: state-of-the-art and outlook, Pervasive Mob. Comput., 5, 1, 110-131, (2009)
[6] Papazoglou, M. P.; van den Heuvel, W., Service oriented architectures: approaches, technologies and research issues, VLDB J., 16, 3, 389-415, (2007)
[7] S. De, T. Elsaleh, P. Barnaghi, S. Meissner, An Internet of Things platform for real-world and digital objects, Scalable Comput. Pract. Exp. 13 (1).
[8] Lanese, I.; Bedogni, L.; Di Felice, M., Internet of things: a process calculus approach, (ACM SAC, (2013), ACM), 1339-1346
[9] Honda, K.; Yoshida, N., On reduction-based process semantics, Theor. Comput. Sci., 151, 2, 437-486, (1995) · Zbl 0871.68122
[10] Sangiorgi, D.; Walker, D., The π-calculus: a theory of mobile processes, (2001), Cambridge University Press · Zbl 0981.68116
[11] van der Schaft, A.; Schumacher, J., An introduction to hybrid dynamical systems, Lect. Notes Control Inf. Sci., vol. 251, (2000), Springer · Zbl 0940.93004
[12] Plotkin, G., A structural approach to operational semantics, (1981), Aarhus University, Report DAIMI FN-19
[13] Hennessy, M.; Regan, T., A process algebra for timed systems, Inf. Comput., 117, 2, 221-239, (1995) · Zbl 0826.68068
[14] Milner, R.; Sangiorgi, D., Barbed bisimulation, (ICALP, Lect. Notes Comput. Sci., vol. 623, (1992), Springer), 685-695
[15] Cerone, A.; Hennessy, M.; Merro, M., Modelling MAC-layer communications in wireless systems, Log. Methods Comput. Sci., 11, 1:18, (2015) · Zbl 1395.94007
[16] Sundararaman, B.; Buy, U.; Kshemkalyani, A., Clock synchronization for wireless sensor networks: a survey, Ad Hoc Netw., 3, 3, 281-323, (2005)
[17] Berry, G.; Gonthier, G., The esterel synchronous programming language: design, semantics, implementation, Sci. Comput. Program., 19, 2, 87-152, (1992) · Zbl 0772.68013
[18] Amadio, R., A synchronous pi-calculus, Inf. Comput., 205, 9, 1470-1490, (2007) · Zbl 1124.68066
[19] Boussinot, F.; de Simone, R., The SL synchronous language, IEEE Trans. Softw. Eng., 22, 4, 256-266, (1996)
[20] Cardelli, L.; Gordon, A., Mobile ambients, Theor. Comput. Sci., 240, 1, 177-213, (2000) · Zbl 0954.68108
[21] Wang, G.; Cao, G.; La Porta, T., Movement-assisted sensor deployment, IEEE Trans. Mob. Comput., 5, 6, 640-652, (2006)
[22] Merro, M.; Zappa Nardelli, F., Behavioral theory for mobile ambients, J. ACM, 52, 6, 961-1023, (2005) · Zbl 1326.68201
[23] Arun-Kumar, S.; Hennessy, M., An efficiency preorder for processes, Acta Inform., 29, 8, 737-760, (1992) · Zbl 0790.68039
[24] Bodei, C.; Degano, P.; Ferrari, G.; Galletta, L., Where do your iot ingredients come from?, (COORDINATION, Lect. Notes Comput. Sci., vol. 9686, (2016), Springer), 35-50
[25] Bodei, C.; Degano, P.; Ferrari, G.; Galletta, L., Tracing where iot data are collected and aggregated, Log. Methods Comput. Sci., 13, 3, 1-38, (2017) · Zbl 1459.68013
[26] Gelernter, D., Generative communication in linda, ACM Trans. Program. Lang. Syst., 7, 1, 80-112, (1985) · Zbl 0559.68030
[27] Lanotte, R.; Merro, M., A calculus of cyber-physical systems, (LATA, vol. 10168, (2017), Springer), 115-127 · Zbl 06725131
[28] R. Lanotte, M. Merro, S. Tini, A probabilistic calculus of cyber-physical systems, CoRR abs/1707.02279. · Zbl 06725131
[29] Lanotte, R.; Merro, M.; Muradore, R.; Viganò, L., A formal approach to cyber-physical attacks, (IEEE CSF, (2017), IEEE Computer Society), 436-450
[30] Lanese, I.; Sangiorgi, D., An operational semantics for a calculus for wireless systems, Theor. Comput. Sci., 411, 1928-1948, (2010) · Zbl 1200.68035
[31] Nanz, S.; Hankin, C., A framework for security analysis of mobile wireless networks, Theor. Comput. Sci., 367, 1-2, 203-227, (2006) · Zbl 1153.68322
[32] Merro, M., An observational theory for mobile ad hoc networks (full paper), Inf. Comput., 207, 2, 194-208, (2009) · Zbl 1165.68052
[33] Godskesen, J., A calculus for mobile ad hoc networks, (COORDINATION, Lect. Notes Comput. Sci., vol. 4467, (2007), Springer), 132-150 · Zbl 1292.68108
[34] Ghassemi, F.; Fokkink, W.; Movaghar, A., Verification of mobile ad hoc networks: an algebraic approach, Theor. Comput. Sci., 412, 28, 3262-3282, (2011) · Zbl 1216.68160
[35] Merro, M.; Ballardin, F.; Sibilio, E., A timed calculus for wireless systems, Theor. Comput. Sci., 412, 47, 6585-6611, (2011) · Zbl 1227.68077
[36] Merro, M.; Sibilio, E., A calculus of trustworthy ad hoc networks, Form. Asp. Comput., 25, 5, 801-832, (2013) · Zbl 1298.68041
[37] Lanotte, R.; Merro, M., Semantic analysis of gossip protocols for wireless sensor networks, (CONCUR, Lect. Notes Comput. Sci., vol. 6901, (2011), Springer), 156-170 · Zbl 1343.68028
[38] Singh, A.; Ramakrishnan, C.; Smolka, S., A process calculus for mobile ad hoc networks, Sci. Comput. Program., 75, 6, 440-469, (2010) · Zbl 1192.68451
[39] Fehnker, A.; van Glabbeek, R.; Höfner, P.; McIver, A.; Portmann, M.; Tan, W., A process algebra for wireless mesh networks, (ESOP, Lect. Notes Comput. Sci., vol. 7211, (2012), Springer), 295-315 · Zbl 1352.68183
[40] Borgström, J.; Huang, S.; Johansson, M.; Raabjerg, P.; Victor, B.; Pohjola, J.; Parrow, J., Broadcast psi-calculi with an application to wireless protocols, Softw. Syst. Model., 14, 1, 201-216, (2015)
[41] Godskesen, J.; Nanz, S., Mobility models and behavioural equivalence for wireless networks, (COORDINATION, Lect. Notes Comput. Sci., vol. 5521, (2009), Springer), 106-122
[42] Vigo, R.; Nielson, F.; Nielson Broadcast, H., Denial-of-service, and secure communication, (IFM, Lect. Notes Comput. Sci., vol. 7940, (2013), Springer), 412-427
[43] Wu, X.; Zhu, H., Formal analysis of a calculus for WSNs from quality perspective, Sci. Comput. Program., (2018), in press
[44] Attar, P.; Castellani, I., Fine-grained and coarse-grained reactive noninterference, (TGC, Lect. Notes Comput. Sci., vol. 8358, (2013), Springer), 159-179 · Zbl 1348.68155
[45] De Nicola, R.; Loreti, M.; Pugliese, R.; Tiezzi, F., A formal approach to autonomic systems programming: the SCEL language, ACM Trans. Auton. Adapt. Syst., 9, 1-29, (2014)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.