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 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.
6. Conclusions and related work
We have proposed a process calculus, called CaIT, to investigate the semantic theory of networked systems in the Internet of Things paradigm. The dynamics of CaIT is formalised by means of an intuitive reduction semantics and (a more operational) labelled intensional semantics that model the evolution of systems in isolation. An Harmony theorem shows that these two different operational semantics coincide. An extensional semantics has then been defined to emphasise the interaction of IoT systems with the environment. The extensional semantics has been used to define a labelled bisimilarity which has been proved to be a coinductive characterisation of a natural notion of contextual equivalence. Our bisimilarity has been used to prove non-trivial system equalities.
To our knowledge, Lanese et al.’s IoT-calculus [8] is the first process calculus for IoT systems capturing the interaction between sensors, actuators and computing processes. Smart objects are represented as point-to-point communicating nodes of heterogeneous networks. The network topology is represented as a graph whose links can be nondeterministically established or destroyed. The paper contains a labelled transition system with two different kinds of transitions. The first one takes into account interactions with the physical environment, similarly to our physical transitions, but includes also topology changes. The second kind of transition models nodes activities, mainly communications, similarly to our logical transitions. The paper proposes two notions of bisimilarity: one using only the first kind of transitions and equating systems from the point of view of the end user, and a second one using all transitions and equating systems from the point of view of the other devices.
