# A Semantic Theory of the Internet of Things

Ruggero Lanotte, Massimo Merro

► To cite this version:

Ruggero Lanotte, Massimo Merro. A Semantic Theory of the Internet of Things. 18th International Conference on Coordination Languages and Models (COORDINATION), Jun 2016, Heraklion, Greece. pp.157-174, 10.1007/978-3-319-39519-7_10 . hal-01631725

HAL Id: hal-01631725

https://inria.hal.science/hal-01631725

Submitted on 9 Nov 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A Semantic Theory of the Internet of Things
(extended abstract)

Ruggero Lanotte<fnref n="1" /> and Massimo Merro<fnref n="2" />

**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.

## 1 Introduction

In the *Internet of Things* (IoT) paradigm, *smart devices*, such as smartphones, automatically collect information from shared resources (e.g. Internet access or physical devices) and aggregate them to provide new services to end users [13]. The “things” commonly deployed in IoT systems are: *RFID tags*, for unique identification, *sensors*, to detect physical changes in the environment, and *actuators*, to pass information to the environment.

The research on IoT is currently focusing on practical applications such as the development of enabling technologies, ad hoc architectures, semantic web technologies, and cloud computing [13]. However, as pointed out by Lanese et al. [16], there is a lack of research in formal methodologies to model the interactions among system components, and to verify the correctness of the network deployment before its implementation.

The main goal of this paper is to propose a process calculus with a clearly-defined semantic theory, for specifying and reasoning on IoT applications. Designing a calculus for modelling a new paradigm requires understanding and distilling, in a clean algebraic setting, the main features of the paradigm. Let us try to figure out what the main ingredients of IoT are, by means of an example.

Suppose a simple *smart home* (see Fig. 1) in which the user can use her smartphone to remotely control the heating boiler of her house, and automatically turn on lights when entering a room. The house consists of an entrance and a lounge, separated by a patio. Entrance and lounge have their own lights (actuators) which are governed by different light manager processes, *LightMng*. The boiler is in the patio and is governed by a boiler manager process, *BoilerMng*. This process senses the local temperature (via a sensor) and decides whether to turn on/off the boiler, setting a proper actuator to signal the state of the boiler.

<footnote n="1">¹ Dipartimento di Scienza e Alta Tecnologia, Università dell'Insubria, Como, Italy</footnote>

<footnote n="2">² Dipartimento di Informatica, Università degli Studi di Verona, Italy</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1 A simple smart home</figcaption></figure>

The smartphone executes two concurrent processes: *BoilerCtrl* and *LightCtr*.
The first one reads user's commands, submitted via the phone touchscreen (a
sensor), and forward them to the process *BoilerMng*, via an Internet channel.
Whereas, the process *LightCtrl* interacts with the processes *LightMng*, via
short-range wireless channels (e.g. Bluetooth), to automatically turn on lights
when the smartphone physically enters either the entrance or the lounge.

The whole system is given by the parallel composition of the smartphone (a
mobile device) and the smart home (a stationary entity).

On this kind of systems one may wish to prove interesting *run-time properties*.
Think of a *fairness* property saying that the boiler will be eventually turned
on/off whenever specific conditions are satisfied. Or consistency properties, saying
the smartphone will never be in two rooms at the same time. Even more, one
may be interested in understanding whether our system has the same *observable
behaviour* of another system. Let us consider a variant of our smart home, where
lights functionality depends on GPS coordinates of the smartphone (localisation
is a common feature of today smartphones). Intuitively, the smartphone sends
its GPS position to a centralised light manager, *CLightMng* (possibly placed in
the patio), via an Internet channel. The process *CLightMng* will then interact
with the two processes *LightMng*, via short-range channels, to switch on/off
lights, depending on the position of the smartphone. Here comes an interesting
question: Can these two implementations of the smart home, based on different
light management mechanisms, be actually distinguished by an end user?

In the paper at hand we develop a fully abstract semantic theory for a
process calculus of IoT systems, called *CaIT*. We provide a formal notion of
when two systems in *CaIT* are indistinguishable, in all possible contexts, from
the point of view of the end user. Formally, we adopt the approach of [15, 24],
often called *reduction (closed) barbed congruence*, which relies on two crucial
concepts: a *reduction semantics* to describe system computations, and the *basic
observables* to represent what the environment can directly observe of a system.
In *CaIT*, there are at least two possible observables: the ability to transmit along
channels, *logical observation*, and the capability to diffuse messages via actuators,
*physical observation*. We have adopted the second form as our contextual equality
remains invariant when adding logical observation. However, the right definition
of physical observation is far from obvious as it involves some technical challenges
in the definition of the reduction semantics (see the discussion in Sec. 2.3).

Our calculus is equipped with two *labelled transition semantics* (LTS) in the
SOS style of Plotkin: an *intensional* semantics and an *extensional* semantics. The
adjective intensional is used to stress the fact that the actions here correspond to
activities which can be performed by a system in isolation, without any interaction with the external environment. While, the extensional semantics focuses on those activities which require a contribution of the environment. We prove that the reduction semantics coincides with the intensional semantics (Harmony Theorem), and that they satisfy some desirable time properties such as *time determinism*, *patience*, *maximal progress* and *well-timedness* [14].

However, the main result of the paper is that weak *bisimilarity* in the extensional LTS is *sound* and *complete* with respect to our contextual equivalence, reduction barbed congruence. This required a non-standard proof of the congruence theorem (Thm. 2). Finally, in order to show the effectiveness of our bisimulation proof method, we prove a number of non-trivial system equalities.

In this extended abstract proofs are omitted; full details can be found in [7].

*Outline* Sec. 2 contains the calculus together with the reduction semantics, the contextual equivalence, and a discussion on design choices. Sec. 3 gives the details of our smart home example, and proves desirable run-time properties for it. Sec. 4 defines both the intensional and the extensional LTS. In Sec. 5 we define bisimilarity for IoT-systems, and prove the full abstraction result together with a number of non-trivial system equalities. Sec. 6 discusses related work.

## 2 The calculus

The syntax of our *Calculus of the Internet of Things*, shortly *CaIT*, is given in a two-level structure: a lower one for *processes* and an upper one for *networks* of smart devices.

$$ 
\begin{array}{lclcl}
M, N & ::= & \mathbf{0} & | & n[\mathcal{I} \times P]^\mu_l & | & M | N | (\nu c)M \\
P, Q & ::= & \mathit{nil} & | & \rho.P & | & P | Q & | & [\pi.P]Q & | & [b]P; Q & | & X & | & \mathit{fix} \ X.P
\end{array}
$$

We use letters *n*, *m* to denote *nodes-devices*, *c*, *g* for *channels*, *l*, *h*, *k* for (physical) *locations*, *s*, *s'* for *sensors*, *a*, *a'* for *actuators* and *x*, *y*, *z* for *variables*. Our *values*, ranged over by *v* and *w*, are constituted by basic values, such as booleans and integers, sensor and actuator values, and coordinates of physical locations.

A network *M* is a pool of *distinct nodes* running in parallel and living in physical locations. We assume a discrete notion of *distance* between two locations *h* and *k*, i.e. $d(h, k) \in \mathbb{N}$. We write *0* to denote the empty network, while *M* | *N* represents the parallel composition of two networks *M* and *N*. In $(\nu c)M$ channel *c* is private to the nodes of *M*. Each node is a term of the form $n[\mathcal{I} \times P]^\mu_l$, where *n* is the device ID; $\mathcal{I}$ is the physical interface of *n*, represented as a partial mapping from sensor and actuator names to physical values; *P* is the process modelling the logics of *n*; *l* is the physical location of the device; $\mu \in \{\mathbf{s}, \mathbf{m}\}$ is a tag to distinguish between stationary and mobile nodes.

For security reasons, sensors in $\mathcal{I}$ can be read only by its *controller process* *P*. Similarly, actuators in $\mathcal{I}$ can be modified only by *P*. No other devices can access the physical interface of *n*. *P* is a timed concurrent processes which manages both the interaction with the physical interface $\mathcal{I}$ and channel communication. The communication paradigm is *point-to-point* via channels that may have different transmission ranges. We assume a global function *rng()* from channel names
to $N \cup \{-1, \infty\}$. A channel $c$ can be used for: i) intra-node communications, if $\text{rang}(c) = -1$; ii) short-range inter-node communications (such as Bluetooth, infrared, etc) if $0 \le \text{rang}(c) < \infty$; iii) Internet communications, if $\text{rang}(c) = \infty$.

Technically, our processes build on CCS with discrete time [14]. We write $\rho.P$, with $\rho \in \{\sigma, \text{@}(x), s?(x), a!v\}$, to denote intra-node actions. The process $\sigma.P$ sleeps for one time unit. The process $\text{@}(x).P$ gets the current location of the enclosing node. Process $s?(x).P$ reads a value $v$ from sensor $s$. Process $a!v.P$ writes the value $v$ on the actuator $a$. We write $\lfloor\pi.P\rfloor Q$, with $\pi \in \{\bar{c}\langle v\rangle, c(x)\}$, to denote channel communication with timeout. This process can communicate in the current time interval and then continues as $P$; otherwise, after one time unit, it evolves into $Q$. We write $[b]P; Q$ for conditional (here guard $\llbracket b \rrbracket$ is always decidable). In processes of the form $\sigma.Q$ and $\lfloor\pi.P\rfloor Q$ the occurrence of $Q$ is said to be time-guarded. The process fix $X.P$ denotes time-guarded recursion, as all occurrences of the process variable $X$ may only occur time-guarded in $P$. In processes $\lfloor c(x).P \rfloor Q$, $s?(x).P$ and $\text{@}(x).P$ the variable $x$ is said to be bound. Similarly, in process fix $X.P$ the process variable $X$ is bound. In the term $(\nu c)M$ the channel $c$ is bound. This gives rise to the standard notions of free/bound (process) variables, free/bound channels, and $\alpha$-conversion. A term is said to be closed if it does not contain free (process) variables, although it may contain free channels. We always work with closed networks: the absence of free variables is preserved at run-time. We write $T\{v/x\}$ for the substitution of the variable $x$ with the value $v$ in any expression $T$ of our language. Similarly, $T\{P/X\}$ is the substitution of the process variable $X$ with the process $P$ in $T$.

Actuator names are metavariables for actuators like `display@n` or `alarm@n`. As node names are unique so are actuator names: different nodes have different actuators. The sensors embedded in a node can be of two kinds: location-dependent and node-dependent. The first ones sense data at the current location of the node, whereas the second ones sense data within the node, independently on the node's location. Thus, node-dependent sensor names are metavariables for sensors like `touchscreen@n` or `button@n`; whereas a sensor `temp@h`, for temperature, is a typical example of location-dependent sensor. Node-dependent sensor names are unique. This is not the case of location-dependent sensor names which may appear in different nodes. For simplicity, we use the same metavariables for both kind of sensors. When necessary we will specify the type of sensor in use.

We rule out ill-formed networks by means of the following definition.

**Definition 1.** A network $M$ is said to be well-formed if: (i) it does not contain two nodes with the same name; (ii) different nodes have different actuators and different node-dependent sensors; (iii) for each $n[\mathcal{I} \times P]_h^\mu$ in $M$, with a prefix $s?(x)$ (resp. $a!v$) in $P$, $\mathcal{I}(s)$ (resp. $\mathcal{I}(a)$) is defined; (iv) for each $n[\mathcal{I} \times P]_h^\mu$ in $M$ with $\mathcal{I}(s)$ defined for some location-dependent sensor $s$, it holds that $\mu = \mathbf{s}$.

Last condition says that location-dependent sensors may be used only in stationary nodes (see discussion in Sec. 2.3). Hereafter, we will always work with *well-formed networks*. It is easy to show that *well-formedness* is preserved at runtime.

We adopt the following notational conventions. $\prod_{i \in I} M_i$ denotes the parallel composition of all $M_i$, for $i \in I$. $\prod_{i \in I} M_i = \mathbf{0}$ and $\prod_{i \in I} P_i = \text{nil}$, for $I = \emptyset$. We write $\prod_i M_i$ when $I$ is not relevant. We write $\pi.P$ instead of $\text{fix} \times X. \lfloor \pi.P \rfloor X$. We use $(\nu \tilde{c})M$ as an abbreviation for $(\nu c_1) \dots (\nu c_k)M$, with $\tilde{c} = c_1, \dots, c_k$.
<table><caption>**Table 1 Reduction semantics**</caption><tr><td>(pos)</td><td>-<br>n[<i>I</i> &times; @<i>(x)</i>.<i>P</i>]<sub><i>h</i></sub><sup>&mu;</sup> &rarr; &tau;<br>n[<i>I</i> &times; P{<sup><i>h</i></sup>/<sub><i>x</i></sub>}]<sub><i>h</i></sub><sup>&mu;</sup> (sensread)</td><td><i>I</i>(<i>s</i>) = <i>v</i><br>n[<i>I</i> &times; s?<i>(x)</i>.<i>P</i>]<sub><i>h</i></sub><sup>&mu;</sup> &rarr; &tau;<br>n[<i>I</i> &times; P{<sup><i>v</i></sup>/<sub><i>x</i></sub>}]<sub><i>h</i></sub><sup>&mu;</sup></td></tr><tr><td>(actunchg)</td><td><i>I</i>(<i>a</i>) = <i>v</i><br>n[<i>I</i> &times; a!<i>v</i>.<i>P</i>]<sub><i>h</i></sub><sup>&mu;</sup> &rarr; &tau;<br>n[<i>I</i> &times; P]<sub><i>h</i></sub><sup>&mu;</sup> (actchg)</td><td><i>I</i>(<i>a</i>) &ne; <i>v</i><br><i>I'</i> := <i>I</i>[<i>a</i> &mapsto; <i>v</i>]<br>n[<i>I</i> &times; a!<i>v</i>.<i>P</i>]<sub><i>h</i></sub><sup>&mu;</sup> &rarr; <i>a</i><br>n[<i>I'</i> &times; P]<sub><i>h</i></sub><sup>&mu;</sup></td></tr><tr><td>(loccom)</td><td><i>rng</i>(<i>c</i>) = -1<br>n[<i>I</i> &times; [<i>c</i>&#x0305;<i>v</i>].<i>P</i>]<i>R</i> | [<i>c</i><i>(x)</i>.<i>Q</i>]<i>S</i>]<sub><i>h</i></sub><sup>&mu;</sup> &rarr; &tau;<br>n[<i>I</i> &times; P | <i>Q</i>{<sup><i>v</i></sup>/<sub><i>x</i></sub>}</i>]<sub><i>h</i></sub><sup>&mu;</sup></td><td></td></tr><tr><td>(timestat)</td><td>n[<i>I</i> &times; &prod;<sub><i>i</i></sub>[<i>&pi;</i><sub><i>i</i></sub>.<i>P</i><sub><i>i</i></sub>]<i>Q</i><sub><i>i</i></sub> | &prod;<sub><i>j</i></sub> <i>&sigma;</i>.<i>R</i><sub><i>j</i></sub>]<sub><i>h</i></sub><sup>s</sup> &ne; &tau;<br>n[<i>I</i> &times; &prod;<sub><i>i</i></sub>[<i>&pi;</i><sub><i>i</i></sub>.<i>P</i><sub><i>i</i></sub>]<i>Q</i><sub><i>i</i></sub> | &prod;<sub><i>j</i></sub> <i>&sigma;</i>.<i>R</i><sub><i>j</i></sub>]<sub><i>h</i></sub><sup>s</sup> &rarr; &sigma;<br>n[<i>I</i> &times; &prod;<sub><i>i</i></sub><i>Q</i><sub><i>i</i></sub> | &prod;<sub><i>j</i></sub><i>R</i><sub><i>j</i></sub>]<sub><i>h</i></sub><sup>s</sup></td><td></td></tr><tr><td>(timemob)</td><td>n[<i>I</i> &times; &prod;<sub><i>i</i></sub>[<i>&pi;</i><sub><i>i</i></sub>.<i>P</i><sub><i>i</i></sub>]<i>Q</i><sub><i>i</i></sub> | &prod;<sub><i>j</i></sub> <i>&sigma;</i>.<i>R</i><sub><i>j</i></sub>]<sub><i>h</i></sub><sup>m</sup> &ne; &tau;<br>d(<i>h</i>, <i>k</i>) &le; &delta;<br>n[<i>I</i> &times; &prod;<sub><i>i</i></sub>[<i>&pi;</i><sub><i>i</i></sub>.<i>P</i><sub><i>i</i></sub>]<i>Q</i><sub><i>i</i></sub> | &prod;<sub><i>j</i></sub> <i>&sigma;</i>.<i>R</i><sub><i>j</i></sub>]<sub><i>h</i></sub><sup>m</sup> &rarr; &sigma;<br>n[<i>I</i> &times; &prod;<sub><i>i</i></sub><i>Q</i><sub><i>i</i></sub> | &prod;<sub><i>j</i></sub><i>R</i><sub><i>j</i></sub>]<sub><i>k</i></sub><sup>m</sup></td><td></td></tr><tr><td>(glbcom)</td><td>d(<i>h</i>, <i>k</i>) &le; <i>rng</i>(<i>c</i>)<br>n[<i>I</i> &times; [<i>c</i>&#x0305;<i>v</i>].<i>P</i>]<i>R</i>]<sub><i>h</i></sub><sup>&mu;1</sup> | m[<i>I</i> &times; [<i>c</i><i>(x)</i>.<i>Q</i>]<i>S</i>]<sub><i>k</i></sub><sup>&mu;2</sup> &rarr; &tau;<br>n[<i>I</i> &times; P]<sub><i>h</i></sub><sup>&mu;1</sup> | m[<i>I</i> &times; <i>Q</i>{<sup><i>v</i></sup>/<sub><i>x</i></sub>}</i>]<sub><i>k</i></sub><sup>&mu;2</sup></td><td></td></tr><tr><td>(parp)</td><td>&prod;<sub><i>i</i></sub><i>n</i><sub><i>i</i></sub>[<i>I</i><sub><i>i</i></sub> &times; <i>P</i><sub><i>i</i></sub>]<sub><i>h</i></sub><sup>&mu;<i>i</i></sup> &rarr; &omega;<br>&prod;<sub><i>i</i></sub><i>n</i><sub><i>i</i></sub>[<i>I'</i><sub><i>i</i></sub> &times; <i>P'</i><sub><i>i</i></sub>]<sub><i>h</i></sub><sup>&mu;<i>i</i></sup> &omega; &isin; {&tau;, <i>a</i>}</td><td>(parn) <i>M</i> &rarr; &omega; <i>M'</i> &omega; &isin; {&tau;, <i>a</i>}</td></tr><tr><td>(timepar)</td><td><i>M</i> &rarr; &sigma;<br><i>N</i> &rarr; &sigma;<br><i>M</i> | <i>N</i> &ne; &tau;<br><i>M'</i> | <i>N'</i></td><td>(timezero) <sup>-</sup><br><i>0</i> &rarr; &sigma;<br><i>0</i></td></tr><tr><td>(res)</td><td><i>M</i> &rarr; &omega;<br><i>N</i> &omega; &isin; {&tau;, <i>a</i>, <i>&sigma;</i>}</td><td><i>M</i> &equiv; <i>N</i><br><i>N</i> &rarr; &omega;<br><i>N'</i> &omega; &isin; {&tau;, <i>a</i>, <i>&sigma;</i>}</td></tr><tr><td>(<i>&nu;</i>c)<i>M</i> &rarr; &omega; (<i>&nu;</i>c)<i>N</i></td><td>(struct) <i>M</i> &rarr; &omega;<br><i>M'</i></td><td><i>M</i> &rarr; &omega;<br><i>M'</i></td></tr></table>

## 2.1 Reduction semantics

The dynamics of the calculus is specified in terms of *reduction relations* over networks (see Tab. 1). As usual in process calculi, a reduction semantics [22] relies on an auxiliary standard relation, ≡, called *structural congruence*, which brings the participants of a potential interaction into contiguous positions. For lack of space, we omit the formal definition of ≡, as it is quite standard.

As C<sub>AIT</sub> is a timed calculus, with a discrete notion of time, it will be necessary to distinguish between *instantaneous reductions*, $M \to_i N$, and *timed reductions*, $M \to_\sigma N$. Relation $\to_i$ denotes activities which take place within one time interval, whereas $\to_\sigma$ represents the passage of one time unit. Instantaneous reductions are of two kinds: those which involve the change of the values associated to some actuator *a*, written $\to_a$, and the others, written $\to_\tau$. Intuitively, reductions of the form $M \to_a N$ denote *watchpoints* which cannot be ignored by the physical environment (in Ex. 2, and more extensively at the end of Sec. 2.3, we explain why this is important). Thus, we define the instantaneous reduction relation $\to_i = \to_\tau \cup \to_a$, for any actuator *a*. We also define the reduction $\to = \to_\tau \cup \to_\sigma$.

The first seven rules in Tab. 1 model intra-node activities. Rule (pos) serves to compute the current position of a node. Rule (sensread) represents the reading
of the current data detected at some sensor *s*. Rules (actunchg) and (actchg) implement the writing of some data *v* on an actuator *a*, distinguishing whether the value of the actuator changes or not. Rule (loccom) models intra-node communications on a local channel *c* (*rng*(*c*) = -1). Rule (timestat) models the passage of time within a stationary node. Notice that all untimed intra-node actions are considered urgent actions as they must occur before the next timed action. Rule (timemob) models the passage of time for mobile nodes. This rule also serves to model *node mobility*. Mobile nodes can nondeterministically move from one physical location *h* to a (possibly different) location *k*, at the end of a time interval. Node mobility respects the following time discipline: in one time unit a node can move from *h* to *k* provided that *d*(*h*, *k*) ≤ *δ*, for some fixed *δ* ∈ N (if *h* = *k* then *d*(*h*, *k*) = 0). For the sake of simplicity, we fix the same constant *δ* for all nodes of our systems. Rule (glbcom) models inter-node communication along a global channel *c* (*rng*(*c*) ≥ 0). Intuitively, two nodes can communicate via a channel *c* only if they are within the transmission range of *c*. Rules (parp) and (parn) serve to propagate instantaneous reductions through parallel processes, and parallel networks, respectively. Rule (timepar) is for inter-node time synchronisation. The remaining rules are standard.

We write $\rightarrow_i^k$ to denote $k$ consecutive reductions $\rightarrow_i$; $\rightarrow_i^*$ is the reflexive and transitive closure of $\rightarrow_i$. We use the same notation for the reduction relation $\rightarrow$.

Below we report a few standard time properties which hold in our calculus: *time determinism*, *maximal progress*, *patience* and *well-timedness*.

**Proposition 1 (Time properties).**

- If $M \rightarrow_{\sigma} M'$ and $M \rightarrow_{\sigma} M''$, then $M' \equiv \prod_{i \in I} n_i [I_i \boxtimes P_i]_{h_i}^{\mu_i}$ and $M'' \equiv \prod_{i \in I} n_i [I_i \boxtimes P_i]_{k_i}^{\nu_i}$, with $d(h_i, k_i) \le 2\delta$, for all $i \in I$.

- If $M \rightarrow_i M'$, then there is no $M''$ such that $M \rightarrow_{\sigma} M''$.

- If $M \rightarrow_i M'$ for no $M'$, then there is $N$ such that $M \rightarrow_{\sigma} N$.

- For any $M$ there is a $z \in \mathbb{N}$ such that if $M \rightarrow_i^u N$ then $u \le z$.

In its standard formulation, time determinism says that a system reaches at most one new state by executing a reduction step $\rightarrow_{\sigma}$. However, by an application of Rule (timemob), our mobile nodes may change location when executing a reduction $\rightarrow_{\sigma}$. *Well-timedness* ensures the absence of infinite instantaneous traces which would prevent the passage of time.

## 2.2 Behavioural equivalence

Our contextual equivalence is *reduction barbed congruence* [15, 24], a standard contextually defined process equivalence that crucially relies on the definition of *basic observables* to represent what the environment can directly observe of a system<fnref n="3" />. As already said in the Introduction, we choose to observe the capability to publish messages via actuators (physical observation).

<footnote n="3">³ See [24] for a comparison between this approach and the original barbed congruence.</footnote>
**Definition 2 (Barbs).** We write $M \downarrow_{a@h!v}$ if $M \equiv (\nu\tilde{g})(n[I \times P]_h^\mu | M')$, with $I(a) = v$. We write $M \downarrow_{a@h!v}$ if $M \to^* M' \downarrow_{a@h!v}$.

The reader may wonder why our barb reports the location and not the node of the actuator. We also recall that actuator names are unique so they somehow codify the name of their node. The location is then necessary because the environment is potentially aware of its position when observing an actuator: if every day at 6.00AM your smartphone rings to wake you up, then you may react differently depending whether you are at home or on holidays in the Bahamas!

**Definition 3.** A binary relation $\mathcal{R}$ over networks is barb preserving if $MRN$ and $M \downarrow_{a@h!v}$ implies $N \downarrow_{a@h!v}$.

**Definition 4.** A binary relation $\mathcal{R}$ over networks is reduction closed if whenever $MRN$ the following conditions are satisfied:

- $M \to M'$ implies $N \to^* N'$ and $M' \mathcal{R} N'$

- $M \to_a M'$ implies $N \to^* \to_a N'$ and $M' \mathcal{R} N'$.

Here, we require reduction closure of both $\to$ and $\to_a$, for any $a$. This is a crucial design decision in CAIT (see Ex. 2 and Sec. 2.3 for details).

In order to model sensor updates made by the physical environment on a sensor $s$, in a given location $h$, we define the operator $[s@h \mapsto v]$ on networks.

**Definition 5.** Given a location $h$, a sensor $s$, and a value $v$, we define:

$$n[I \times P]_h^\mu [s@h \mapsto v] \stackrel{\text{def}}{=} n[I[s \mapsto v] \times P]_h^\mu, \text{ if } \mathcal{I}(s) \text{ defined}$$

$$n[I \times P]_k^\mu [s@h \mapsto v] \stackrel{\text{def}}{=} n[I \times P]_k^\mu, \text{ if } \mathcal{I}(s) \text{ undef. or } h \neq k$$

$$(M | N)[s@h \mapsto v] \stackrel{\text{def}}{=} M[s@h \mapsto v] | N[s@h \mapsto v]$$

$$((\nu c)M)[s@h \mapsto v] \stackrel{\text{def}}{=} (\nu c)(M[s@h \mapsto v])$$

$$\mathbf{0}[s@h \mapsto v] \stackrel{\text{def}}{=} \mathbf{0}.$$

Notice that when updating a sensor we use its location, also for node-dependent sensors. This is because when changing a node-dependent sensor (e.g. touching a touchscreen of a smartphone) the environment is in general aware of its position.

**Definition 6.** A binary relation $\mathcal{R}$ is contextual if $MRN$ implies that

- for all networks $O, M | O \mathcal{R} N | O$

- for all channels $c, (\nu c)M \mathcal{R} (\nu c)N$

- for all $s, h$, and $v$ in the domain of $s$, $M[s@h \mapsto v] \mathcal{R} N[s@h \mapsto v]$.

The first two clauses requires closure under logical contexts (parallel systems), while the last clause involves physical contexts, which can nondeterministically update sensor values.

Finally, everything is in place to define our touchstone behavioural equality.

**Definition 7.** Reduction barbed congruence, $\cong^b$, is the largest symmetric relation over networks which is reduction closed, barb preserving and contextual.
*Remark 1.* Obviously, if $M \cong N$ then $M$ and $N$ will be still equivalent in any setting where sensor updates are governed by specific physical laws.

We recall that the reduction relation $\rightarrow$ ignores the passage of time, and therefore the reader might suspect that our reduction barbed congruence is impervious to the precise timing of activities. We show that this is not the case.

*Example 1.* Let $M = n[\emptyset \bowtie \sigma. [\bar{c}(\langle)] \mathbf{nil}]_h^s$ and $N = n[\emptyset \bowtie [\bar{c}(\langle)] \mathbf{nil}]_h^s$, with $\text{rang}(c) = \infty$. Then, $M \rightarrow_{\sigma} N$. As $\rightarrow$ does not distinguish instantaneous from timed reductions, one may suspect that $M \cong N$, and that a prompt transmission along channel $c$ is equivalent to the same transmission delayed of one time unit. However, the test $T = \text{test}[\mathcal{J} \bowtie \sigma.a!1. [c().a!0] \mathbf{nil}]_l^s$, with $\mathcal{J}(a) = 0$, for some actuator $a$, can distinguish the two networks. In fact, if $M \mid T \rightarrow \rightarrow_a O = n[\emptyset \bowtie [\bar{c}(\langle)] \mathbf{nil}]_h^s \mid \text{test}[\mathcal{J}' \bowtie [c().a!0] \mathbf{nil}]_l^s$, with $\mathcal{J}'(a) = 1$, then there is no $O'$ such that $N \mid T \rightarrow^{*} \rightarrow_a \rightarrow^{*} O'$ with $O \cong O'$. This is because $O$ can perform a reduction sequence $\rightarrow \rightarrow_a$ that cannot be matched by any $O'$.

Behind this example there is the general principle that reduction barbed congruence is sensitive to the passage of time.

**Proposition 2.** If $M \cong N$ and $M \rightarrow_{\sigma} M'$ then there is $N'$ such that $N \rightarrow_{\tau}^{*} \rightarrow_{\sigma} \rightarrow_{\tau}^{*} N'$ and $M' \cong N'$.

Now, we provide some insights into the design decision of having two different instantaneous reductions $\rightarrow_{\tau}$ and $\rightarrow_a$.

*Example 2.* Let $M=n[\mathcal{I} \bowtie a!1 \mid a!0.a!1]_h^\mu$ and $N=n[\mathcal{I} \bowtie a!1.a!0.a!1]_h^\mu$, with $\mathcal{I}(a)=0$ and undefined otherwise. Then, within one time unit, $M$ may display on the actuator $a$ either the sequence of values 01 or the sequence 0101, while $N$ can only display the sequence 0101. As a consequence, for a physical observer, the behaviours of $M$ and $N$ are clearly different. Now, if $M \rightarrow_{\tau} \rightarrow_a M' = n[\mathcal{J} \bowtie a!1]_h^\mu$, with $\mathcal{J}(a) = 1$, the only possible reply of $N$ respecting reduction closure is $N \rightarrow^{*} \rightarrow_a N' = n[\mathcal{J} \bowtie a!0.a!1]_h^\mu$. However, it is evident that $M' \not\cong N'$ because $N'$ can turn the actuator $a$ to 0 while $M'$ cannot. Thus, $M \not\cong N$.

Had we merged $\rightarrow_a$ with $\rightarrow_{\tau}$ then we would have $M \cong N$ because the capability to observe messages on actuators, given by the barb, would not be enough to observe changes on actuators within one time interval.

## 2.3 Design choices

CaIT is a value-passing process calculus, à la CCS, which can be easily adapted to deal with the transmission of channel names, à la $\pi$-calculus [24].

The time model we adopt is known as the fictitious clock approach (see [14]): a global clock is supposed to be updated whenever all nodes agree on this, by globally synchronising on a special timing action $\sigma$. Thus, time synchronisation relies on some clock synchronisation protocol for mobile wireless systems [27].

In cyber-physical systems [25], sensor changes are usually modelled either using continuous models (differential equations) or through discrete models (difference
equations)$^4$. However, in this paper we aim at providing a behavioural semantics for IoT applications from the point of the view of the end user. And the end user cannot directly observe changes on the sensors of an IoT application: she can only observe the effects of those changes via actuators and communication channels. Thus, in *CaIT* we do not represent sensor changes via specific models, but we rather abstract on them by supporting *nondeterministic sensor updates* (see Def. 5 and 6). Actually, as said in Rem. 1, behavioural equalities derived in our setting remains valid when adopting any specific model for sensor updates.

In *CaIT* the value associated to sensors and actuators can change more than once within the same time interval. At first sight this choice may appear weird as certain actuators may require some time to turn on. On the other hand, other actuators may have a very quick reaction. A similar argument applies to sensors. In this respect *CaIT* does not enforce a synchronisation of physical events as it happens for logical signals in synchronous languages [5]. In fact, actuator changes are under nodes’ control: if an actuator is a slow device then it is under the responsibility of its controller to update the actuator with a proper delay. Similarly, a sensor should be read only when its value makes sense.

Unlike *mobile computations* [6], smart devices do not decide where to move to: an external agent moves them. Furthermore, Def. 1 imposes that location-dependent sensors can only occur in stationary nodes. This allows us a local, rather than a global, representation of those sensors. The representation of mobile location-dependent sensors would have the same technical challenges of *mobile wireless sensor networks* [27].

Finally, we would like to explain our choice of barb. As said in the Introduction there are other possible definitions. For instance, one could observe the capability to transmit along a channel *c*, by defining $M \downarrow_{\bar{c}@h}^c$ if $M \equiv (\nu\tilde{g})(n[\mathcal{I} \bowtie [\bar{c}\langle v\rangle.P]Q | R])_k^\mu | N)$ with $c \notin \tilde{g}$ and $d(h,k) \le \text{rang}(c)$. However, if you consider the system $S = (\nu c)(M | m[\mathcal{J} \bowtie |c(x).a!1]|\text{nil})_h^\mu)$, with $\mathcal{J}(a) = 0$, then it is easy to show that $M \downarrow_{\bar{c}@h}$ if and only if $S \dashv\dashv a S' \downarrow_{a@h!1}$. Thus, the barb on channels can always be reformulated in terms of our barb. The vice versa is not possible. The reader may also wonder whether it is possible to turn the reduction $\dashv a$ into $\dashv_\tau$ by introducing some special barb which would be capable to observe actuators changes. For instance, something like $M \downarrow_{a@h!w}^c$ if $M \equiv (\nu\tilde{g})(n[\mathcal{I} \bowtie a!w.P | Q])_h^\mu | M')$, with $\mathcal{I}(a) = v$ and $v \ne w$. It should be easy to see that this extra barb would not help in distinguishing the terms proposed in Ex. 2. Actually, here there is something deeper that needs to be spelled out. In process calculi, the term $\beta$ of a barb $\downarrow_\beta$ is a concise encoding of a context $C_\beta$ expressible in the calculus and capable to observe the barb $\downarrow_\beta$. However, our barb $\downarrow_{a@h!v}$ does not have such a corresponding *physical context* in our language. Said with an example, in *CaIT* we do not represent the “eyes of a person” looking at the values appearing to some display. Technically speaking, in our calculus we don’t have terms of the form $a?(x).P$ to read values on the actuator *a*, simply because such terms would not be part of an IoT system. The lack of this physical

<footnote n="4">⁴ Difference equations relate to differential equations as discrete math relate to continuous math.</footnote>
<table><caption>**Table 2** A smart home in CaIT</caption><tr><td>Sys</td><td>def=</td><td>Phone | Home</td></tr><tr><td>Phone</td><td>def=</td><td>n<sub>P</sub>[I<sub>P</sub> &times; BoilerCtrl | LightCtrl]<sub>out</sub><sup>m</sup></td></tr><tr><td>Home</td><td>def=</td><td>LM<sub>1</sub> | BM | LM<sub>2</sub></td></tr><tr><td>LM<sub>1</sub></td><td>def=</td><td>n<sub>1</sub>[I<sub>1</sub> &times; LightMng<sub>1</sub>]<sub>loc<sub>1</sub></sub><sup>s</sup></td></tr><tr><td>LM<sub>2</sub></td><td>def=</td><td>n<sub>2</sub>[I<sub>2</sub> &times; LightMng<sub>2</sub>]<sub>loc<sub>4</sub></sub><sup>s</sup></td></tr><tr><td>BM</td><td>def=</td><td>n<sub>B</sub>[I<sub>B</sub> &times; BoilerMng]<sub>loc<sub>2</sub></sub><sup>s</sup></td></tr><tr><td>BoilerCtrl</td><td>def=</td><td>fix X.mode?(z).[b&#773;(z).&sigma;X]&nbsp;X</td></tr><tr><td>LightCtrl</td><td>def=</td><td>&Pi;<sup>2</sup><sub>j=1</sub> fix X.[c&#773;<sub>j</sub>(&#773;)&middot;&sigma;X]&nbsp;X</td></tr><tr><td>LightMng<sub>j</sub></td><td>def=</td><td>fix X.[c<sub>j</sub>().light<sub>j</sub>!on.&sigma;X]&nbsp;light<sub>j</sub>!off.X for j &isin; {1, 2}</td></tr><tr><td>BoilerMng</td><td>def=</td><td>fix X.[b(x).[x = man] boiler!on.&sigma;.Manual; TempCtrl]&nbsp;TempCtrl</td></tr><tr><td>Manual</td><td>def=</td><td>fix Y.b(y).[y = auto]&nbsp;X; &sigma;Y</td></tr><tr><td>TempCtrl</td><td>def=</td><td>temp?(t).[t &lt; &Theta;] boiler!on.&sigma;X; boiler!off.&sigma;X</td></tr></table>

context, together with the persistent nature of actuators' state, explains why our barb $\downarrow_{a@h!v}$ must work together with the reduction relation $\rightarrow_a$ to provide the desired distinguishing power of $\cong$. Further discussions can be found in [7].

### 3 Case study: a smart home

In Tab. 2, we model the smart home discussed in the Introduction, and represented in Fig. 1. Our house spans over 4 contiguous physical locations $loc_i$, for $i = [1..4]$, such that $d(loc_i, loc_j) = |i - j|$. The entrance is in $loc_1$, the patio spans from $loc_2$ to $loc_3$ and the lounge is at $loc_4$. The house can only be accessed via its entrance.

Our system Sys consists of the parallel composition of the smartphone, Phone, and the smart home, Home. The smartphone is represented as a mobile node, with $\delta = 1$, initially placed outside the house: $out \neq loc_j$, for $j \in [1..4]$. As the phone can only access the house from its entrance, and $\delta = 1$, we have $d(l, loc_i) \ge i$, for any $l \notin \{loc_1, loc_2, loc_3, loc_4\}$ and $i \in [1..4]$. Its interface $I_P$ contains only one sensor, called mode, representing the touchscreen to control the boiler. This is a node-dependent sensor. The process BoilerCtrl reads sensor mode and forwards its value to the boiler manager in the patio, BoilerMng, via the Internet channel $b$ ($\text{rang}(b) = \infty$). The domain of mode is $\{\text{man}, \text{auto}\}$, where man stands for manual and auto for automatic; initially, $I_P(\text{mode}) = \text{auto}$.

In Phone there is a second process, called LightCtrl, which allows the smartphone to switch on lights only when getting in touch with the light managers installed in the rooms. Here, channels $c_1$ and $c_2$ serve to control the lights of entrance and lounge, respectively; these are short-range channels: $\text{rang}(c_1) = \text{rang}(c_2) = 0$.

The smart home Home consists of three stationary nodes: $LM_1$, $BM$, and $LM_2$. The light managers processes $LightMng_1$, $LightMng_2$, are placed in $LM_1$ and $LM_2$, respectively. They manage the corresponding lights via the actuators $light_j$, for $j \in \{1, 2\}$. The domain of these actuators is $\{\text{on}, \text{off}\}$; initially, $I_j(light_j) = \text{off}$, for $j \in \{1, 2\}$.
<table><caption>**Table 3** Smart home: a position based light management</caption><tr><td>Sys</td><td>def</td><td>Phone | Home</td></tr><tr><td>Phone</td><td>def</td><td>n<sub>P</sub>[I<sub>P</sub> &times; BoilerCtrl | LightCtrl]<sub>out</sub><sup>m</sup></td></tr><tr><td>Home</td><td>def</td><td>Home | CLM</td></tr><tr><td>CLM</td><td>def</td><td>n<sub>C</sub>[0 &times; CLightMng]<sub>loc3</sub><sup>s</sup></td></tr><tr><td>LightCtrl</td><td>def</td><td>fix X.@(x).[g&#773;(x).&sigma;.X]X</td></tr><tr><td>CLightMng</td><td>def</td><td>fix X.[g(y).[y = loc<sub>1</sub>][c&#773;<sub>1</sub>(&#9675;).&sigma;.X]X; [y = loc<sub>4</sub>][c&#773;<sub>2</sub>(&#9675;).&sigma;.X]X; &sigma;.X]X</td></tr></table>

The boiler manager process *BoilerMng* is placed in *BM* (node *n*<sub>B</sub>). Here, the physical interface *I*<sub>B</sub> contains a sensor named *temp* and an actuator called *boiler*; *temp* is a location-dependent temperature sensor, whose domain is $\mathbb{N}$, and *boiler* is an actuator to display boiler functionality, whose domain is {on, off}. The boiler manager can work either in automatic or in manual mode. In automatic mode, sensor *temp* is periodically checked: if the temperature is under a threshold $\Theta$ then the boiler will be switched on, otherwise it will be switched off. Conversely, in manual mode, the boiler is always switched on. Initially, the boiler is in automatic mode, $I_B(temp) = \Theta$, and $I_B(boiler) = \text{off}$.

Our system Sys enjoys a number of desirable *run-time properties*. For instance, if the boiler is in manual mode or its temperature is under the threshold $\Theta$ then the boiler will get switched on, within one time unit. Conversely, if the boiler is in automatic mode and its temperature is higher than or equal to the threshold $\Theta$, then the boiler will get switched off within one time unit. These three *fairness* properties can be easily proved because our calculus is well-timed. In general, similar properties cannot be expressed in untimed calculi. Finally, our last property states the phone cannot act on the lights of the two rooms at the same time, manifesting a kind of “ubiquity”. For the sake of simplicity, in the following proposition we omit location names both in barbs and in sensor updates, writing $\downarrow_{a!v}$ instead of $\downarrow_{a@h!v}$, and $[s \mapsto v]$ instead of $[s@h \mapsto v]$. The system Sys' denotes an arbitrary (stable) derivative of Sys.

**Proposition 3 (Run-time properties).** Let Sys ($\to_i^* \to_\sigma$) Sys'.

- If Sys'[mode $\mapsto$ man] $\to_i^*$ Sys'' $\to_\sigma$ then Sys'' $\downarrow_{boiler!on}$

- If Sys'[temp $\mapsto$ t] $\to_i^*$ Sys'' $\to_\sigma$, with t < $\Theta$, then Sys'' $\downarrow_{boiler!on}$

- If Sys'[temp $\mapsto$ t] $\to_i^*$ Sys'' $\to_\sigma$, with t $\ge$ $\Theta$, then Sys'' $\downarrow_{boiler!off}$

- If Sys' $\to_i^*$ Sys'' $\downarrow_{light_1!on}$ then Sys'' $\downarrow_{light_2!off}$, and vice versa.

Finally, we propose a variant of our system, where lights functionality depends on the position of the smartphone. Intuitively, the smartphone detects is current GPS position, via the process @(*x*).P, and then sends it to a centralised light manager process, CLightMng, via an Internet channel *g*. This process will interact with the local light managers to switch on/off lights, depending on the position of the smartphone. In Table 3, new components have been overlined. Channels *c*<sub>1</sub> and *c*<sub>2</sub> have different range now, as they serve to communicate with the centralised light manager: *rang*(*c*<sub>1</sub>) = 2 and *rang*(*c*<sub>2</sub>) = 1.

Prop. 3 holds for Sys as well. Actually, the two systems are closely related.
<table><caption>**Table 4** Intensional semantics for processes</caption><tr><td>(SndP) <table style="display: inline-block; vertical-align: middle; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 5px;">[c&#773;&lang;v&rang; &middot; P]</td></tr><tr><td style="padding: 0 5px;">Q</td></tr></tbody></table> Q &rarr; P</td><td>(RcvP) <table style="display: inline-block; vertical-align: middle; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 5px;">[c(x) &middot; P]</td></tr><tr><td style="padding: 0 5px;">Q</td></tr></tbody></table> Q &rarr; P{v/x}</td></tr><tr><td>(PosP) <table style="display: inline-block; vertical-align: middle; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 5px;">@&lang;x&rang; &middot; P</td></tr><tr><td style="padding: 0 5px;">@&lang;h&rang;</td></tr></tbody></table> P{h/x}</td><td>(Com) <table style="display: inline-block; vertical-align: middle; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 5px;">P &rarr; P'</td></tr><tr><td style="padding: 0 5px;">Q &rarr; Q'</td></tr></tbody></table> Q' &rarr; Q' &nbsp;&nbsp;&nbsp; rng(c) = -1<br>P | Q &rarr; P' | Q'</td></tr><tr><td>(Sensor) <table style="display: inline-block; vertical-align: middle; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 5px;">s?&lang;x&rang; &middot; P</td></tr><tr><td style="padding: 0 5px;">s?v</td></tr></tbody></table> P{v/x}</td><td>(Actuator) <table style="display: inline-block; vertical-align: middle; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 5px;">a!v &middot; P</td></tr><tr><td style="padding: 0 5px;">a!v</td></tr></tbody></table> P</td></tr><tr><td>(ParP) <table style="display: inline-block; vertical-align: middle; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 5px;">P &rarr; P'</td></tr><tr><td style="padding: 0 5px;">P | Q</td></tr></tbody></table> &lambda; &ne; &sigma;<br>P | Q &rarr; P' | Q</td><td>(Fix) <table style="display: inline-block; vertical-align: middle; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 5px;">P{fix X &middot; P/X}</td></tr><tr><td style="padding: 0 5px;">&lambda; &rarr; Q</td></tr></tbody></table> &rarr; Q<br>fix X &middot; P &lambda; &rarr; Q</td></tr><tr><td>(TimeNil) <table style="display: inline-block; vertical-align: middle; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 5px;">nil</td></tr><tr><td style="padding: 0 5px;">&sigma;</td></tr></tbody></table> &rarr; nil</td><td>(Delay) <table style="display: inline-block; vertical-align: middle; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 5px;">&sigma; &middot; P</td></tr><tr><td style="padding: 0 5px;">&sigma;</td></tr></tbody></table> P</td></tr><tr><td>(Timeout) <table style="display: inline-block; vertical-align: middle; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 5px;">[&pi; &middot; P]</td></tr><tr><td style="padding: 0 5px;">Q</td></tr></tbody></table> Q &rarr; Q</td><td>(TimeParP) <table style="display: inline-block; vertical-align: middle; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 5px;">P &rarr; P'</td></tr><tr><td style="padding: 0 5px;">Q &rarr; Q'</td></tr></tbody></table> Q' &rarr; P | Q &ne; P' | Q'</td></tr></table>

**Proposition 4.** For $\delta = 1$, $(\nu\tilde{c})Sys \cong (\nu\tilde{c})(\nu g)\overline{Sys}$.

The bisimulation proof technique developed in the remainder of the paper will be very useful to prove equalities between systems of such size.

We end this section with a comment. While reading this case study the reader should have noticed that our reduction semantics does not model sensor updates. This is because sensor changes depend on the physical environment, and a reduction semantics models the evolution of a system in isolation. Interactions with the external environment will be treated in our *extensional semantics*.

# 4 Labelled transition semantics

In this section we provide two labelled semantic models in the SOS style of Plotkin: the *intensional semantics* and the *extensional semantics*.

*Intensional semantics* Since our syntax distinguishes between networks and processes, we have two different kinds of transitions:

- $P \xrightarrow{\lambda} Q$, with $\lambda \in \{\sigma, \tau, \bar{c}v, cv, @h, s?v, a!v\}$, for *process transitions*

- $M \xrightarrow{\nu} N$, with $\nu \in \{\sigma, \tau, a, \bar{c}v@h, cv@h\}$, for *network transitions*.

In Tab. 4 we report transition rules for processes, very much in the style of [14]. As in CCS, we assume $[b]P; Q = P$ if $[[b]] = true$, and $[b]P; Q = Q$ if $[[b]] = false$. Rules (SndP), (RcvP) and (Com) model communications along a channel c. Rule (PosP) is for extracting the physical position of the embedding node. Rules (Sensor) and (Actuator) serve to read sensors, and to write on actuators, respectively. Rules (ParP) and (Fix) are straightforward. The remaining rules allow us to derive the timed action $\sigma$. In Rule (Delay) a timed prefix is consumed. Rule (Timeout)
<table><caption>**Table 5** Intensional semantics for networks</caption><tr><td>(Pos)</td><td>P <sub>h</sub> <sup>@h</sup>→ P'<br>n[I×P]<sub>h</sub><sup>μ</sup> <sub>τ</sub>→ n[I×P']<sub>h</sub><sup>μ</sup></td><td>(SensRead)</td><td>I(s) = v P <sub>h</sub> <sup>s?v</sup>→ P'<br>n[I×P]<sub>h</sub><sup>μ</sup> <sub>τ</sub>→ n[I×P']<sub>h</sub><sup>μ</sup></td></tr><tr><td>(ActUnChg)</td><td>I(a) = v P <sub>h</sub> <sup>a!v</sup>→ P'<br>n[I×P]<sub>h</sub><sup>μ</sup> <sub>τ</sub>→ n[I×P']<sub>h</sub><sup>μ</sup></td><td>(LocCom)</td><td>P <sub>h</sub> <sup>τ</sup>→ P'<br>n[I×P]<sub>h</sub><sup>μ</sup> <sub>τ</sub>→ n[I×P']<sub>h</sub><sup>μ</sup></td></tr><tr><td>(ActChg)</td><td>I(a) ≠ v P <sub>h</sub> <sup>a!v</sup>→ P'<br>n[I×P]<sub>h</sub><sup>μ</sup> <sub>a</sub>→ n[I×P']<sub>h</sub><sup>μ</sup></td><td></td><td>I' := I[a ↦ v]<br>n[I×P]<sub>h</sub><sup>μ</sup> <sub>a</sub>→ n[I×P']<sub>h</sub><sup>μ</sup></td></tr><tr><td>(TimeStat)</td><td>P <sub>h</sub> <sup>σ</sup>→ P'<br>n[I×P]<sub>h</sub><sup>s</sup> <sub>σ</sub>→ n[I×P']<sub>h</sub><sup>s</sup></td><td>(TimeMob)</td><td>P <sub>h</sub> <sup>σ</sup>→ P'<br>n[I×P]<sub>h</sub><sup>m</sup> <sub>σ</sub>→ n[I×P']<sub>h</sub><sup>m</sup></td></tr><tr><td>(Snd)</td><td>P <sub>h</sub> <sup>cv</sup>→ P'<br>n[I×P]<sub>h</sub><sup>μ</sup> <sub>cv@h</sub>→ n[I×P']<sub>h</sub><sup>μ</sup></td><td>(Rcv)</td><td>P <sub>h</sub> <sup>cv</sup>→ P'<br>n[I×P]<sub>h</sub><sup>μ</sup> <sub>cv@h</sub>→ n[I×P']<sub>h</sub><sup>μ</sup></td></tr><tr><td>(GlbCom)</td><td>M <sub>h</sub> <sup>cv@k</sup>→ M'<br>N <sub>h</sub> <sup>cv@h</sup>→ N'<br>M | N <sub>τ</sub>→ M' | N'</td><td></td><td>d(h, k) ≤ rng(c)</td></tr><tr><td>(ParN)</td><td>M <sub>h</sub> <sup>ν</sup>→ M'<br>M | N <sub>ν</sub>→ M' | N</td><td>(TimePar)</td><td>M <sub>h</sub> <sup>σ</sup>→ M'<br>M | N <sub>σ</sub>→ M' | N'</td></tr><tr><td>(TimeZero)</td><td>0 <sub>σ</sub>→ 0</td><td>(Res)</td><td>M <sub>h</sub> <sup>ν</sup>→ N<br>ν ∉ {cv@h, cv@h}<br>(νc)M <sub>ν</sub>→ (νc)N</td></tr></table>

models timeouts when channel communications are not possible in the current time interval. Rule (TimeParP) is for time synchronisation of parallel processes. The symmetric counterparts of Rules (ParP) and (Com) are omitted.

In Tab. 5 we report the rules for networks. Rule (Pos) extracts the position of a node. Rule (SensRead) models the reading of a sensor of the enclosing node. Rules (ActUnChg) and (ActChg) describes the writing of a value $v$ on an actuator $a$ of the node, distinguishing whether the value of the actuator is changed or not. Rule (LocCom) models intra-node communications. Rule (TimeStat) models the passage of time for a stationary node. Rule (TimeMob) models both time passing and node mobility at the end of a time interval. Rules (Snd) and (Rcv) model transmission and reception along an global channel. Rule (GlbCom) models inter-node communications. The remaining rules are straightforward. The symmetric counterparts of Rules (ParN) and (GlbCom) are omitted.

The reduction semantics and the labelled intensional semantics coincide.

**Theorem 1 (Harmony theorem).** Let $\omega \in \{\tau, a, \sigma\}$:

$$- M \xrightarrow{\omega} M' \text{ implies } M \dashv\omega M'$$

$$- M \dashv\omega M' \text{ implies } M \xrightarrow{\omega} M'', \text{ for some } M'' \text{ such that } M' \equiv M''.$$

**Extensional semantics** Here we redesign our LTS to focus on the interactions of our systems with the external environment. As the environment has a *logical*
The proof that $\approx$ is preserved by the sensor update operator $[s@h \mapsto v]$ is non-standard and technically challenging. It required a well-founded induction.

Thm. 2 is crucial to prove that our bisimilarity is sound with respect to reduction barbed congruence. Actually, our bisimilarity is both sound and complete.

**Theorem 3 (Full abstraction).** $M \approx N$ iff $M \cong N$.

Soundness follows from Thm. 1, Thm. 2, and the capability of extensional actions to capture barbs. As to completeness, for any extensional action $\alpha$ we exhibit an observing context $C_\alpha$.

*Remark 2.* A consequence of Thm. 3 and Rem. 1 is that our bisimulation proof-technique remains sound in a setting with more restricted contexts, where nonterministic sensor updates are replaced by some specific model for sensors.

As testbed for our notion of bisimilarity, we prove a number of algebraic laws on well-formed networks.

**Theorem 4 (Some algebraic laws).**

1. $n[I \times a!v.P \mid R]^\mu_h \gtrsim n[I \times P \mid R]^\mu_h$, if $I(a) = v$ and a does not occur in $R$

2. $n[I \times @ (x).P \mid R]^\mu_h \gtrsim n[I \times \{h/x\}P \mid R]^\mu_h$

3. $n[I \times [\bar{c}\langle v \rangle.P]S \mid [c(x).Q]T \mid R]^\mu_h \gtrsim n[I \times P \mid Q^{v/x} \mid R]^\mu_h$, $c$ not in $R$ and $\text{rang}(c)=-1$

4. $(\nu c)(n[I \times [\bar{c}\langle v \rangle.P]S \mid R]^\mu_h \mid m[J \times [c(x).Q]T \mid U]^\mu_k)$
$$ \gtrsim (\nu c)(n[I \times P \mid R]^\mu_h \mid m[J \times Q^{v/x} \mid U]^\mu_k), \text{ if } \text{rang}(c) = \infty \text{ and } c \text{ does not occur in } R \text{ and } U $$

5. $n[I \times P]^\mu_h \gtrsim n[I \times \text{nil}]^\mu_h$, if subterms $\lfloor \pi.P_1 \rfloor P_2$ or $a!v.P_1$ do not occur in $P$

6. $n[I \times \text{nil}]^\mu_h \approx 0$, if $I(a)$ is undefined for any actuator $a$

7. $n[0 \times P]^\mu_h \approx m[0 \times P]^\mu_k$, if $P$ does not contain terms of the form $@ (x).Q$, and for any channel $c$ in $P$ either $\text{rang}(c) = \infty$ or $\text{rang}(c) = -1$.

Laws 1-4 are a sort of tau-laws. Laws 5 and 6 models garbage collection of processes and nodes, respectively. Law 7 gives a sufficient condition for node anonymity as well as for non-observable node mobility.

Finally, we show that our labelled bisimilarity can be used to deal with more complicated systems. Let us prove that the two variants of the smart home mentioned in Prop. 4 are actually bisimilar.

**Proposition 5.** If $\delta = 1$ then $(\nu \tilde{c})\text{Sys} \approx (\nu \tilde{c})(\nu g)\overline{\text{Sys}}$.

Due to the size of the systems involved, the proof of the proposition above is quite challenging. In this respect, the first four laws of Thm. 4 are fundamentals to apply non-trivial up-to expansion proof-techniques [24].

# 6 Related work

To our knowledge, the IoT-calculus [16] is the first (and only) process calculus for IoT systems. We report here the main differences between CaIT and the IoT-calculus. In CaIT, we can express desirable time and runtime properties (see Prop. 1 and Prop. 3). The nondeterministic link entailment of the IoT-calculus
makes communication simpler than ours; on the other hand it does not allow to
enforce that a smart device cannot be in two places at the same time. In *CaIT*,
both sensors and actuators are under the control of a single entity, i.e. the process
of the node where they were deployed. This was a security issue. *CaIT* has a
finer control of inter-node communication: it takes into account both distance
among nodes and transmission range of channels. Node mobility in *CaIT* is timed
constrained: in one time unit at most a fixed distance *δ* may be covered.

Finally, Lanese et al. equip the IoT-calculus with an *end-user bisimilarity*
which shares the same motivations of our bisimilarity. In the IoT-calculus, end
users provide values to sensors and check actuators. Unlike us, they can also
observe node mobility but they cannot observe channel communication. End-
user bisimilarity is not preserved by parallel composition. Compositionality is
recovered by strengthening its discriminating power.

Our calculus takes inspiration from algebraic models for wireless systems [17, 23, 19, 12, 3, 18, 20, 11, 26, 10, 21, 8, 4]. Most of these models adopt broadcast communication, while we consider point-to-point communication, as in [16, 10, 21]. We model network topology as in [17, 19]. Prop. 2 was inspired by [8]. Fully abstract observational theories for calculi of wireless systems appear in [12, 19, 8].

Vigo et al. [28] proposed a calculus for *wireless-based cyber-physical systems* endowed with a theory to model and reasoning on cryptographic primitives, together with explicit notions of communication failure and unwanted communication. However, as pointed out in [29], the calculus does not provide a notion of network topology, local broadcast and behavioural equivalence. It also lacks a clear distinction between physical components (sensor and actuators) and logical ones (processes). Compared to [28], paper [29] introduces a static network topology and enrich the theory with an harmony theorem.

CaIT shares some similarities with the *synchronous languages* of the Esterel family [5]. In synchronous languages, computations proceed in phases called instants, which have some similarity with our time intervals. For instance, our timed reduction semantics has some points in common with that of *CRL* [2].

Finally, CaIT is somehow reminiscent of the SCEL language [9]. A framework
to model behaviour, knowledge, and data aggregation of Autonomic Systems.

*Acknowledgements* We thank Ilaria Castellani and Matthew Hennessy for their precious comments, and Valentina Castiglioni for an early proof of the harmony theorem. The anonymous referees provided useful comments.

References

1. Arun-Kumar, S., Hennessy, M.: An efficiency preorder for processes. Acta Informatica 29, 737-760 (1992)

2. 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 (2013)

3. 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. Borgström, J., Huang, S., Johansson, M., Raabjerg, P., Victor, B., Pohjola, J., Parrow, J.: Broadcast psi-calculi with an application to wireless protocols. Software and System Modeling 14(1), 201–216 (2015)
5. Boussinot, F., de Simone, R.: The SL synchronous language. IEEE Transactions on Software Engineering 22(4), 256-266 (1996)

6. Cardelli, L., Gordon, A.: Mobile ambients. TCS 240(1), 177-213 (2000)

7. Castiglioni, V., Lanotte, R., Merro, M.: A Semantic Theory of the Internet of Things. CoRR abs/1510.04854 (2015)

8. Cerone, A., Hennessy, M., Merro, M.: Modelling mac-layer communications in wireless systems. Logical Methods in Computer Science 11(1:18) (2015)

9. De Nicola, R., Loreti, M., Pugliese, R., Tiezzi, F.: A Formal Approach to Autonomic Systems Programming: The SCEL language. ACM TAAS 9, 7:1-7:29 (2014)

10. Fehnker, A., van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., Tan, W.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 295-315. Springer, Heidelberg (2012)

11. Ghassemi, F., Fokkink, W., Movaghar, A.: Verification of Mobile Ad Hoc Networks: an Algebraic Approach. TCS 412(28), 3262-3282 (2011)

12. Godskesen, J.: A Calculus for Mobile Ad Hoc Networks. In: Murphy, A.L., Vitek, J. (eds.) COORDINATION 2007. LNCS, vol. 4467, pp. 132-150. Springer (2007)

13. Gubbi, J., Palaniswami, M.: Internet of things (IoT): A vision, architectural elements, and future directions. Fut. Gen. Comput. Syst. 29(7), 1645-1660 (2013)

14. Hennessy, M., Regan, T.: A process algebra for timed systems. Information and Computation 117(2), 221-239 (1995)

15. Honda, K., Yoshida, N.: On reduction-based process semantics. TCS 151(2), 437-486 (1995)

16. 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. Lanese, I., Sangiorgi, D.: An Operational Semantics for a Calculus for Wireless Systems. TCS 411, 1928-1948 (2010)

18. 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)

19. Merro, M.: An Observational Theory for Mobile Ad Hoc Networks (full version). Information and Computation 207(2), 194-208 (2009)

20. Merro, M., Ballardin, F., Sibilio, E.: A timed calculus for wireless systems. TCS 412(47), 6585-6611 (2011)

21. Merro, M., Sibilio, E.: A calculus of trustworthy ad hoc networks. Formal Aspects of Computing 25(5), 801-832 (2013)

22. Milner, R.: The polyadic π-calculus: a tutorial. Tech. rep., LFCS (1991)

23. Nanz, S., Hankin, C.: A Framework for Security Analysis of Mobile Wireless Networks. TCS 367(1-2), 203-227 (2006)

24. Sangiorgi, D., Walker, D.: The Pi-Calculus a theory of mobile processes. Cambridge University Press (2001)

25. Schaft, A., Schumacher, H.: An introduction to hybrid dynamical systems, Lecture Notes in Control and Information Science, vol. 251. Springer, Heidelberg (2000)

26. Singh, A., Ramakrishnan, C., Smolka, S.: A process calculus for Mobile Ad Hoc Networks. SCP 75(6), 440-469 (2010)

27. Sundararaman, B., Buy, U., Kshemkalyani, A.D.: Clock synchronization for wireless sensor networks: a survey. Ad Hoc Networks 3(3), 281-323 (2005)

28. Vigo, R., Nielson, F., Nielson, H.: 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)

29. Wu, X., Zhu, H.: A calculus for wireless sensor networks from quality perspective. In: HASE 2015. pp. 223-231. IEEE Computer Society (2015)