Skip to main content

2016 | OriginalPaper | Buchkapitel

A Semantic Theory of the Internet of Things

(Extended Abstract)

verfasst von : Ruggero Lanotte, Massimo Merro

Erschienen in: Coordination Models and Languages

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

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 represents a fully abstract 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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
See [24] for a comparison between this approach and the original barbed congruence.
 
2
Difference equations relate to differential equations as discrete math relate to continuous math.
 
Literatur
2.
Zurück zum Zitat Attar, P., Castellani, I.: Fine-grained and coarse-grained reactive noninterference. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 159–179. Springer, Heidelberg (2014)CrossRef Attar, P., Castellani, I.: Fine-grained and coarse-grained reactive noninterference. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 159–179. Springer, Heidelberg (2014)CrossRef
3.
Zurück zum Zitat Benetti, D., Merro, M., Vigano, L.: Model checking ad hoc network routing protocols: Aran vs. endairA. In: Fiadeiro, J.L., Gnesi, S., Maggiolo-Schettini, M. (eds.) SEFM 2010. pp. 191–202. IEEE Computer Society (2010) Benetti, D., Merro, M., Vigano, L.: Model checking ad hoc network routing protocols: Aran vs. endairA. In: Fiadeiro, J.L., Gnesi, S., Maggiolo-Schettini, M. (eds.) SEFM 2010. pp. 191–202. IEEE Computer Society (2010)
4.
Zurück zum Zitat 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)CrossRefMATH 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)CrossRefMATH
5.
Zurück zum Zitat Boussinot, F., de Simone, R.: The SL synchronous language. IEEE Trans. Softw. Eng. 22(4), 256–266 (1996)CrossRef Boussinot, F., de Simone, R.: The SL synchronous language. IEEE Trans. Softw. Eng. 22(4), 256–266 (1996)CrossRef
7.
Zurück zum Zitat Castiglioni, V., Lanotte, R., Merro, M.: A Semantic Theory of the Internet of Things. CoRR abs/1510.04854 (2015) Castiglioni, V., Lanotte, R., Merro, M.: A Semantic Theory of the Internet of Things. CoRR abs/1510.04854 (2015)
8.
Zurück zum Zitat Cerone, A., Hennessy, M., Merro, M.: Modelling mac-layer communications in wireless systems. Logical Methods Comput. Sci. 11(1: 18), 1–59 (2015)MathSciNetMATH Cerone, A., Hennessy, M., Merro, M.: Modelling mac-layer communications in wireless systems. Logical Methods Comput. Sci. 11(1: 18), 1–59 (2015)MathSciNetMATH
9.
Zurück zum Zitat De Nicola, R., Loreti, M., Pugliese, R., Tiezzi, F.: A Formal Approach to Autonomic Systems Programming: The SCEL language. ACM TAAS 9(2), 7: 1–7: 29 (2014) De Nicola, R., Loreti, M., Pugliese, R., Tiezzi, F.: A Formal Approach to Autonomic Systems Programming: The SCEL language. ACM TAAS 9(2), 7: 1–7: 29 (2014)
10.
Zurück zum Zitat Fehnker, A., van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 295–315. Springer, Heidelberg (2012)CrossRef Fehnker, A., van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 295–315. Springer, Heidelberg (2012)CrossRef
11.
Zurück zum Zitat Ghassemi, F., Fokkink, W., Movaghar, A.: Verification of mobile ad hoc networks: an algebraic approach. TCS 412(28), 3262–3282 (2011)MathSciNetCrossRefMATH Ghassemi, F., Fokkink, W., Movaghar, A.: Verification of mobile ad hoc networks: an algebraic approach. TCS 412(28), 3262–3282 (2011)MathSciNetCrossRefMATH
12.
Zurück zum Zitat Godskesen, J.C.: A calculus for mobile ad hoc networks. In: Murphy, A.L., Vitek, J. (eds.) COORDINATION 2007. LNCS, vol. 4467, pp. 132–150. Springer, Heidelberg (2007)CrossRef Godskesen, J.C.: A calculus for mobile ad hoc networks. In: Murphy, A.L., Vitek, J. (eds.) COORDINATION 2007. LNCS, vol. 4467, pp. 132–150. Springer, Heidelberg (2007)CrossRef
13.
Zurück zum Zitat Gubbi, J., Palaniswami, M.: Internet of things (IoT): a vision, architectural elements, and future directions. Future Gener. Comput. Syst. 29(7), 1645–1660 (2013)CrossRef Gubbi, J., Palaniswami, M.: Internet of things (IoT): a vision, architectural elements, and future directions. Future Gener. Comput. Syst. 29(7), 1645–1660 (2013)CrossRef
16.
Zurück zum Zitat Lanese, I., Bedogni, L., Di Felice, M.: Internet of things: a process calculus approach. In: Shin, S.Y., Maldonado, J.C. (eds.) SAC 2013, pp. 1339–1346. ACM (2013) Lanese, I., Bedogni, L., Di Felice, M.: Internet of things: a process calculus approach. In: Shin, S.Y., Maldonado, J.C. (eds.) SAC 2013, pp. 1339–1346. ACM (2013)
17.
18.
Zurück zum Zitat Lanotte, R., Merro, M.: Semantic analysis of gossip protocols for wireless sensor networks. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 156–170. Springer, Heidelberg (2011)CrossRef Lanotte, R., Merro, M.: Semantic analysis of gossip protocols for wireless sensor networks. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 156–170. Springer, Heidelberg (2011)CrossRef
19.
21.
22.
Zurück zum Zitat Milner, R.: The polyadic \(\pi \)-calculus: a tutorial. Technical report, LFCS (1991) Milner, R.: The polyadic \(\pi \)-calculus: a tutorial. Technical report, LFCS (1991)
23.
24.
Zurück zum Zitat Sangiorgi, D., Walker, D.: The Pi-Calculus a Theory of Mobile Processes. Cambridge University Press, New York (2001)MATH Sangiorgi, D., Walker, D.: The Pi-Calculus a Theory of Mobile Processes. Cambridge University Press, New York (2001)MATH
25.
Zurück zum Zitat Schaft, A., Schumacher, H.: An Introduction to Hybrid Dynamical Systems. Lecture Notes in Control and Information Science, vol. 251. Springer, Heidelberg (2000)CrossRefMATH Schaft, A., Schumacher, H.: An Introduction to Hybrid Dynamical Systems. Lecture Notes in Control and Information Science, vol. 251. Springer, Heidelberg (2000)CrossRefMATH
26.
Zurück zum Zitat Singh, A., Ramakrishnan, C., Smolka, S.: A process calculus for Mobile Ad Hoc Networks. SCP 75(6), 440–469 (2010)MathSciNetMATH Singh, A., Ramakrishnan, C., Smolka, S.: A process calculus for Mobile Ad Hoc Networks. SCP 75(6), 440–469 (2010)MathSciNetMATH
27.
Zurück zum Zitat Sundararaman, B., Buy, U., Kshemkalyani, A.D.: Clock synchronization for wireless sensor networks: a survey. Ad Hoc Netw. 3(3), 281–323 (2005)CrossRef Sundararaman, B., Buy, U., Kshemkalyani, A.D.: Clock synchronization for wireless sensor networks: a survey. Ad Hoc Netw. 3(3), 281–323 (2005)CrossRef
28.
Zurück zum Zitat Vigo, R., Nielson, F., Nielson, H.R.: Broadcast, denial-of-service, and secure communication. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 412–427. Springer, Heidelberg (2013)CrossRef Vigo, R., Nielson, F., Nielson, H.R.: Broadcast, denial-of-service, and secure communication. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 412–427. Springer, Heidelberg (2013)CrossRef
29.
Zurück zum Zitat Wu, X., Zhu, H.: A calculus for wireless sensor networks from quality perspective. In: HASE 2015, pp. 223–231. IEEE Computer Society (2015) Wu, X., Zhu, H.: A calculus for wireless sensor networks from quality perspective. In: HASE 2015, pp. 223–231. IEEE Computer Society (2015)
Metadaten
Titel
A Semantic Theory of the Internet of Things
verfasst von
Ruggero Lanotte
Massimo Merro
Copyright-Jahr
2016
DOI
https://doi.org/10.1007/978-3-319-39519-7_10