Chiara Bodei
email: chiara@di.unipi.it

Pierpaolo Degano
email: degano@di.unipi.it

Gian-Luigi Ferrari

Letterio Galletta
email: galletta@di.unipi.it

Where do your IoT ingredients come from?

The Internet of Things (IoT) is here: smart objects are pervading our everyday life. Smart devices automatically collect and exchange data of various kinds, directly gathered from sensors or generated by aggregations. Suitable coordination primitives and analysis mechanisms are in order to design and reason about IoT systems, and to intercept the implied technology shifts. We address these issues by defining IoT-LySa, a process calculus endowed with a static analysis that tracks the provenance and the route of IoT data, and detects how they affect the behaviour of smart objects.

Introduction

This is the era of the Internet of Things (IoT), where digitally connected devices are intruding into our everyday life. "Software is eating the world" is the vivid slogan referring to the smartification of the objects and devices around us. As buzzword, the IoT is indeed simple and accurate: a global network of things ranging from light bulbs to cars, equipped with suitable software allowing things to interact each other and coordinate their behaviour. For instance, our smart alarm clock can drive our coffeemaker to prepare us a cup of coffee in the morning, while our smart TV can suggest us some movies for the evening. Furthermore, smart devices can automatically exchange information of various kinds gathered from different sources (e.g. sensors) or generated by aggregating several data sets.

More connected smart devices and more applications available on the IoT mean more software bugs and vulnerabilities to identify and fix. For instance, a bug can cause you to wake up into a cold house in winter or an attacker can enter into your smart TV and break your bank account. This is not a big surprise: every advance in information technology has exposed software to new challenges.

Smart devices exhibit and require open-endedness to achieve full interactive and cooperative behaviour, and thus they generalise the so-called "embedded systems." These are essentially controllers of machines and are closed systems. Therefore, we cannot simply rely on standard techniques for supporting the design and development of IoT, and new software solutions have emerged, e.g. Amazon AWS for IoT and Google Brillo. We argue that the formal techniques and tools need to be adapted in order to support open-endedness of IoT applications and the new complex phenomena that arise in this hybrid scenario.

Here, we contribute to this new line of research by introducing the kernel of a formal design framework for IoT, which will provide us with the foundations to develop verification techniques and tools for certifying properties of IoT applications.

Our starting point is the process calculus IoT-LySa, a dialect of LySa [START_REF] Bodei | Static validation of security protocols[END_REF][START_REF] Buchholtz | A calculus for control flow analysis of security protocols[END_REF], within the process calculi approach to IoT [START_REF] Lanese | Internet of things: a process calculus approach[END_REF][START_REF] Castiglioni | A semantic theory for the internet of things[END_REF]. It has primitive constructs to describe the activity of sensors and of actuators, and suitable primitives for managing the coordination and communication capabilities of smart objects. More precisely, our calculus is made up from:

1. systems of nodes, consisting of (a representation of) the physical components, i.e. sensors and actuators, and of software control processes for specifying the logic of the node, including the manipulation of data gathered from sensors and from other nodes. Intra-node generative communications are implemented through a shared store à la Linda [START_REF] Gelernter | Generative communication in linda[END_REF][START_REF] Carriero | A computational model of everything[END_REF]. The adoption of this coordination model supports a smooth implementation of the cyber-physical control architecture: physical data are made available to software entities that analyse them and trigger the relevant actuators to perform the desired behaviour. 2. an asynchronous multi-party communication among nodes, which can be easily tuned to take care of various constraints, mainly those concerning proximity; 3. functions to process and aggregate data.

A further contribution of this paper is the definition of an analysis for IoT-LySa to statically predict the run time behaviour of smart systems. We introduce a Control Flow Analysis (CFA) that safely approximates the abstract behaviour of a system of nodes. Essentially, it describes the interactions among nodes, tracks how data spread from sensors to the network, and how data are manipulated.

Technically, our CFA abstracts from the concrete values and only considers their provenance and how they are put together. In more detail, it returns for each node in the network:

an abstract store Σ that records for sensors and variables a super-set of the abstract values that they may denote at run time; a set κ( ) that over-approximates the set of the messages received by the node , and for each of them its sender; a set Θ( ) of possible abstract values computed and used by the node .

The result of the analysis can be exploited as the basis for checking and certifying various properties of IoT systems. As it is, the components κ and Θ track how data may flow in the network and how they influence the outcome of functions. An example of property that can be statically checked using the component κ is the detection of redundant communications, thus providing the means for refactoring the system to avoid message storms. Further, the analysis can be used to check whether the values produced by a certain classified sensor reaches an untrusted node. This helps evaluating the security level of the system and detecting potential vulnerabilities. The paper is organised as follows. The next section introduces our approach with the help of an illustrative example. In Sect. 3 we briefly introduce the process calculus IoT-LySa, while we present our CFA in Sect. 4. Concluding remarks and related work are in Sect. 5.

A smart street light control system

The IoT European Research Cluster (IERC) has recently identified smart lighting in smart cities [START_REF]IERC: The Internet of Things 2012 -New Horizons[END_REF] as one of most relevant applications for the Internet of Things. Recent studies, e.g. [START_REF] Elejoste | An easy to deploy street light control system based on wireless communication and led technology[END_REF][START_REF] Escolar | Estimating energy savings in smart street lighting by using an adaptive control system[END_REF], show that smart street light control systems represent effective solutions to improve energy efficiency. Many proposed solutions are based on sensors that acquire data about the physical environment and regulate the level of illumination according to the detected events. In this section we show how this kind of scenario can be easily modelled in IoT-LySa and what kind of information our CFA provides to designers.

We consider a simplified system made of two integrated parts, working on a one-way street. The first consists of smart lamp posts that are battery powered and can sense their surrounding environment and can communicate with their neighbours to share their views. If (a sensor of) the lamp post perceives a pedestrian and there is not enough light in the street it switches on the light and communicates the presence of the pedestrian to the lamp posts nearby. When a lamp post detects that the level of battery is low, it informs the supervisor of the street lights, N s , that will activate other lamp posts nearby. The second component of the street light controller uses the electronic access point to the street. When a car crosses the checkpoint, besides detecting if it is enabled to, a message is sent to the supervisor of the street accesses, N a , that in turn notifies the presence of the car to N s . This supervisor sends a message to the lamp post closest to the checkpoint that starts a forward chain till the end of the street. The structure of our control light system is in Fig. 1.

We first define the checkpoint N cp as an IoT-LySa node that only contains a visual sensor S cp to take a picture of the car detected in the street, defined as

S cp = µh.(τ.1 := v p ).τ. h
where v p is the picture of the car. The sensor communicates the picture to the node by storing it in the location 1 of the shared store. In our model we assume that each sensor has a reserved store location in which records its readings. The action τ denotes internal actions of the sensor, which we are not interested to model, e.g. reading from the environment; the construct µh. implements the iterative behaviour of the sensor. Then, the taken picture is enhanced by the process P cp and sent to the supervisor N a

P cp = µh.(z := 1).(z := noiseRed(z)). z { a }. h
where a is the label of the node N a (note that 1 is the identifier of the sensor S cp in the assignment z := 1). Hence, the checkpoint N cp is defined as

N cp = cp : [P cp S cp B cp ]
where cp is the identifier of N cp and B cp abstracts other components we are not interested in. The node N a (checks if the car is allowed to enter the street and) communicates its presence to the lamp posts supervisor N s :

N a = a : [ µh.(; x). car, x { s }. h B a ]
where s is the identifier of N s (see below for the intuition of the general format of the input (; x)). The supervisor N s contains the process P s,1 that receives the picture from N a and sends a message to the node closest to the checkpoint, call it N 1 , labelled with 1 :

P s,1 = µh.(car; x). x { 1 }. h
The input (car; x) is performed only if the corresponding output matches the constant car, and the store variable x is bound to the value of the second element of the output (see below for the full definition of N s ).

In our intelligent street light control system there is a node N p for each lamp post, each of which has a unique identifier p ∈ [1, k]. The lamp posts have four sensors to sense (1) the environment light, (2) the solar light, (3) the battery level and (4) the presence of a pedestrian. Each of them is defined as follows

S p,i = µ h. (i := v). τ. h
where v is the perceived value and i ∈ [START_REF] Abadi | A calculus for cryptographic protocols: The Spi calculus[END_REF][START_REF] Bodei | Static validation of security protocols[END_REF] are the store locations for the sensors. After some internal actions τ , the sensor S p,i iterates its behaviour. The actuator for the lamp post p is defined as

A 5 = µ h. (|5, {turnon, turnoff}|). h
It only accepts a message from N c whose first element is its identifier (here 5) and whose second element is either command turnon or turnoff and executes it.

The control process of a lamp post node is composed by two parallel processes. The first process P p,1 is defined as follow

P p,1 = µh.(x 1 := 1. x 2 := 2. x 3 := 3. x 4 := 4). (x 4 = true) ? (x 1 ≤ th 1 ∧ x 2 ≤ th 2 ) ? (x 3 ≥ th 3 ) ? 5, turnon . x 4 L p . h : err, p { s }. h : h : 5, turnoff . h
The process reads the current values from the sensors and stores them into the local variables x i . The actuator is turned on if (i) a pedestrian is detected in the street (x 4 holds), (ii) the intensity of environment and solar lights are greater than the given thresholds th 1 and th 2 , and (iii) there is enough battery (at least th 3 ). In addition, the presence of the pedestrian is communicated to the lamp posts nearby, whose labels, typically p-1 and p+1 , are in L p . Instead, if the level battery is insufficient, an error message, including its identifier p , is sent to the supervisor node, labelled s . The second process P p,2 is defined as follows:

P p,2 = µh.(; x). (x = true ∨ is a car(x)) ? ( 5, turnon . x L p ).h : 5, turnoff . h
It waits for messages from its neighbours or from the supervisor node N s . When one of them is notified the presence of a pedestrian (x = true) or of a car (is a car(x) holds), the current lamp post orders the actuator to switch the light on. Each lamp post p is described as the IoT-LySa node below:

N p = p : [Σ p P p,1 P p,2 S p,1 S p,2 S p,3 S p,4 A p,5 ]
where Σ p is the store of the node p , shared with its components. The supervisor node N s of lamp posts is defined as

N s = s : [µh. (err; x). true L x . h P s,1 B s ]
where P s,1 is the process previously defined. As above the input (err; x) is performed only if the corresponding output matches the constant err, and the store variable x is bound to the value of the second element of the output i.e. the label of the relevant lamp post. If this is the case, after some internal elaborations N s warns the lamp posts nearby x (included in L x ) of the presence of a pedestrian. Therefore, the whole intelligent controller N of the street lights is described as the parallel composition of the checkpoint node N cp , the supervisors nodes N a and N s , and the nodes of lamp posts N p , with p ∈ [1, k]:

N = N cp | N a | N s | N 1 | • • • | N k
We would like to statically predict how the system behaves at run time. In particular, we want to compute: (i) how nodes interact each other; (ii) how data spread from sensors to the network (tracking); and (iii) which computations each node performs on the received data. To do that, we define a Control Flow Analysis (CFA), which abstracts from the concrete values by only considering their provenance and how they are manipulated. Consider e.g. the picture sent by the camera of S cp to its control process P pc . In the analysis we are only interested in tracking where the picture comes from, and not in its actual value; so we use the abstract value 1 cp to record the camera that took it. The process P pc reduces the noise in the pictures and sends the result to N a . Our analysis keeps track of this manipulation through the abstract value noiseRed cp (1 cp ), meaning that the function noiseRed, computed by the node cp , is applied to data coming from the sensor with identifier 1 of cp .

In more detail, our CFA returns for each node in the network: an abstract store Σ that records for each variable a super-set of the abstract values that it may denote at run time; a set κ( ) that approximates the set of the messages received by the node ; and the set Θ( ) of possible abstract values computed and used by the node .

In our example, for each lamp post labelled p , the analysis returns in κ( p ) both the abstract value noiseRed cp (1 cp ) and the sender of that message, i.e.

p+1 . The result of our analysis can be exploited to perform several verifications. For instance, since the pictures of cars are sensitive data, one would like to check whether they are kept secret. By inspecting κ and Θ we discover that the sensitive data of cars is sent to all lamp posts, so possibly violating privacy. Another example is detecting whether there are redundant communications, e.g. since the street is one-way, when a car is present the lamp post at position p needs not to alert the one at p -1. From κ it is easy to detect a redundant communication from the next lamp post.

The calculus IoT-LySa

We adapt the LySa calculus [START_REF] Bodei | Automatic validation of protocol narration[END_REF][START_REF] Bodei | Static validation of security protocols[END_REF][START_REF] Buchholtz | A calculus for control flow analysis of security protocols[END_REF], based on the π- [START_REF] Milner | A calculus of mobile processes[END_REF] and Spi-calculus [START_REF] Abadi | A calculus for cryptographic protocols: The Spi calculus[END_REF], to model IoT applications. For that we introduce: (i) systems of nodes, in turn consisting of sensors, actuators and control processes, plus a shared store Σ within each node for internal communications; (ii) primitives for reading from sensors, and for triggering actuator actions; (iii) an asynchronous multi-party communication modality among nodes, subject to constraints, mainly concerning proximity; (iv) functions to process data; (v) explicit conditional statements. For brevity, we do not include here encryption and decryption primitives as in LySa.

Syntax. Systems have a two-level structure and consist of a fixed number of labelled nodes, hosting a store, control processes, sensors and actuators. The label uniquely identifies the node : [B] and may represent further characterising information (e.g. its location or other contextual information). Finally, the operator | describes a node system of nodes obtained by parallel composition. The syntax of nodes is as follows.

N N ::= systems of nodes 0 inactive node : [B] single node ( ∈ L, the set of labels)

N 1 | N 2
parallel composition of nodes

B B ::= node components Σ node store P process S
sensor, with a unique identifier i ∈ I A actuator, with a unique identifier i ∈ J B B parallel composition of node components

We impose that in : [B] there is a single store Σ : X ∪ I → V, where X , V are the sets of variables and of values, respectively. Our store is essentially an array of fixed dimension, so intuitively a variable is the index in the array and an index i ∈ I corresponds to a single sensor (no need of α-conversions). We assume that store accesses are atomic, e.g. through CAS instructions [START_REF] Herlihy | Wait-free synchronization[END_REF]. The other node components are obtained by the parallel composition of control processes P , and of a fixed number of (less than #(I )) sensors S, and actuators A (less than #(J )). The syntax of processes is as follows

P P ::= control processes 0 inactive process E 1 , • • • , E k L. P asynchronous multi-output L⊆ L (E 1 , • • • , E j ; x j+1 , • • • , x k
). P input (with matching) E?P : Q conditional statement h iteration variable µh. P tail iteration x := E. P assignment to x ∈ X j, γ . P output of action γ to actuator j

The prefix E 1 , • • • , E k L implements a simple form of multi-party communication among nodes: the tuple E 1 , . . . , E k is asynchronously sent to the nodes with labels in L and that are "compatible" (according, among other attributes, to a proximity-based notion). The input prefix (

E 1 ,• • •, E j ; x j+1 ,• • •, x k )
is willing to receive a k-tuple, provided that its first j elements match the input ones, and then binds the remaining store variables (separated by a ";") to the corresponding values (see [START_REF] Buchholtz | A calculus for control flow analysis of security protocols[END_REF][START_REF] Bodei | Static evidences for attack reconstruction[END_REF] for a more flexible choice). Otherwise, the k-tuple is not accepted. A process repeats its behaviour, when defined through the tail iteration construct µh. P , where h is the iteration variable.

A sensor can perform an internal action τ or store the value v, gathered from the environment, into its store location i. An actuator can perform an internal action τ or execute one of its action γ, possibly received from its controlling process. Both sensors and actuators can iterate. For simplicity, here we neither provide an explicit operation to read data from the environment, nor to describe the impact of actuator actions on the environment. Sensors and actuators (uniquely labelled) have the form: The syntax of terms follows.

E E ::= terms v value (v ∈ V) i sensor location (i ∈ I ) x variable (x ∈ X ) f (E 1 , • • • , E n ) function on data The term f (E 1 , • • • , E n )
is the application of function f to n arguments; we assume given a set of primitive functions, typically for aggregating or comparing values, be them computed or representing data in the environment.

Operational Semantics. Our reduction semantics assumes the following structural congruence ≡ on nodes, processes and sensors. It is standard except for the last rule that equates a multi-output with no receivers to the inactive process.

-(N / ≡ , |, 0) and (B/ ≡ , , 0) are commutative monoids -µ h . X ≡ X{µ h . X/h} for X ∈ {P, A, S}

-E 1 , • • • , E k : ∅. 0 ≡ 0
We have a two-level reduction relation defined as the least relation on nodes and its components, denoted by →, satisfying the set of inference rules in Table 1. We assume the standard denotational interpretation [[E]] Σ for evaluating terms.

The first two rules implement the (atomic) asynchronous update of shared variables inside nodes, by using the standard notation Σ{-/-}. According to (S-store), the i th sensor uploads the value v, gathered from the environment, into the store location i. According to (Asgm), a control process updates the variable x with the value of E. The rules (Ev-out) and (Multi-com) drive asynchronous multi-communications among nodes. In the first a node labelled willing to send a tuple of values v 1 , ..., v k , obtained by the evaluation of E 1 , ..., E k , spawns a new process, running in parallel with the continuation P ; its task is to offer the evaluated tuple to all its receivers L. In the rule (Multi-com), the message coming from 1 is received by a node labelled 2 . The communication succeeds, provided that (i) 2 belongs to the set L of possible receivers, (ii) the two nodes are compatible according to the compatibility function Comp, and (iii) that the first j values match with the evaluations of the first j terms in the input.

(S-store)

Σ i := v. Si B → Σ{v/i} Si B (Asgm) [[E]]Σ = v Σ x := E. P B → Σ{v/x} P B (Ev-out) V k i=1 vi = [[Ei]]Σ Σ E1, • • • , E k L. P B → Σ v1, • • • , v k L.0 P B (Multi-com) 2 ∈ L ∧ Comp( 1, 2) ∧ V j i=1 vi = [[Ei]]Σ 2 1 : [ v1, • • • , v k L. 0 B1] | 2 : [Σ2 (E1, • • • , Ej; xj+1, • • • , x k ).Q B2] → 1 : [ v1, • • • , v k L \ { 2}. 0 B1] | 2 : [Σ2{vj+1/xj+1, • • • , v k /x k } Q B2] (Cond) [[E]]Σ = bi Σ E? P1 : P2 B → Σ Pi B where b1 = true, b2 = false (A-com) γ ∈ Γ j, γ . P (|j, Γ |). A B → P γ. A B (Act) γ.A → A (Int) τ. X → X (Node) B → B : → : [B ] (ParN) N1 → N 1 N1|N2 → N 1 |N2 (ParB) B1 → B 1 B1 B2 → B 1 B2 (CongrY) Y 1 ≡ Y1 → Y2 ≡ Y 2 Y 1 → Y 2
Table 1. Reduction semantics, where X ∈ {S, A} and Y ∈ {N, B}.

Moreover, the label 2 is removed by the set of receivers L of the tuple. The spawned process terminates when all its receivers have received the message (see the last congruence rule). The role of the compatibility function Comp is crucial in modelling real world constraints on communication. A basic requirement is that inter-node communications are proximity-based, i.e. that only nodes that are in the same transmission range can directly exchange messages. This is easily encoded here by defining a predicate (over node labels) yielding true only when two nodes are in the same transmission range. Of course, this function could be enriched in order to consider finer notions of compatibility expressing various policies, e.g. topics for event notification. Note that if Comp varies along time, we recover a simple way of expressing dynamic network topologies. According to the evaluation of the expression E, the rule (Cond) says that the process continues as P 1 (if [[E]] Σ is true) or as P 2 (otherwise). A process commands the j th actuator through the rule (A-com), by sending it the pair j, γ ; γ prefixes the actuator, if it is one of its actions. The rule (Act) says that the actuator performs the action γ. Similarly, for the rules (Int) for internal actions. The last rules propagate reductions across parallel composition ((ParN) and (ParB)) and nodes (Node), while the (CongrY) are the standard reduction rules for congruence.

Control Flow Analysis

Our CFA aims at safely approximating the abstract behaviour of a system of nodes N . The analysis follows the same schema of that for LySa [START_REF] Bodei | Static validation of security protocols[END_REF], and for the time being we only conjecture that computing its results requires the same low polynomial time complexity. Here, we track the usage of sensor values inside the local node where they are gathered and their propagation in the network of nodes both as raw data or processed via suitable functions. We resort to abstract values for sensor and functions on abstract values, as follows, where ∈ L:

V v ::= abstract terms special abstract value denoting cut i sensor abstract value (i ∈ I ) v node abstract value f (v 1 , • • • , vn ) function on abstract data
Since the dynamic semantics may introduce function terms with an arbitrarily nesting level, we have new special abstract values that denote all those function terms with a depth greater that a given d. In the clauses defining our analysis, we will used to keep the maximal depth of abstract terms less or equal to d, defined as expected. Note that, once given the set of functions f occurring in a node N , the abstract values are finitely many.

The result of our CFA is a triple ( Σ, κ, Θ) (a pair ( Σ, Θ) for terms E, resp.), called estimate for N (for E, resp.), that satisfies the judgements defined by the rules of Tables 3 and2. For this we introduce the following abstract domains:

abstract store Σ = ∈L Σ : X ∪ I → 2 V where each abstract local store Σ approximates the concrete local store Σ , by associating with each location a set of abstract values that represent the possible concrete values that the location may store at run time.

abstract network environment κ :

L → L × k i=1
Vi (with Vi+1 = V × Vi and k maximum arity of messages), that includes all the messages that may be received by the node labelled .

abstract data collection Θ : L → 2 V that, for each node labelled , approximates the set of values that the node computes.

For each term E, the judgement ( Σ, Θ) |= E : ϑ, defined by the rules in Table 2, expresses that ϑ ∈ V is an acceptable estimate of the set of values that E may evaluate to in Σ . A sensor identifier and a value evaluate to the set ϑ, provided that their abstract representations belong to ϑ. Similarly a variable x evaluates to ϑ, if this includes the set of values bound to x in Σ . The last rule analyses

As it is, our analysis tracks the actual usage of sensor data through the component Θ. It is straightforward to also detect which actions of actuators are actually triggered. The result might suggest to use a simpler actuator if some of its actions are never exercised, or even to remove it if it is never used. Technically, a new analysis component α suffices, that for every actuator j collects the actions γ triggered by the control process in the node . Then, one has only to change the rule for the command to the actuator, as follows:

γ ∈ α (j) ∧ ( Σ, κ, α, Θ) |= P ( Σ, κ, α, Θ) |= j, γ . P
To improve the precision of our CFA, we can refine the abstract store by replacing it with the pair Σin , Σout , similarly to the treatment of side effects in [START_REF] Nielson | Flow logic: A multi-paradigmatic approach to static analysis[END_REF]. This extension is more invasive, because it requires modifying the rules for accurately handling the store updates. We can obtain a further improvement of the precision by making the analysis more context-sensitive. In particular, an additional component can record the sequence of choices made in conditionals while traversing the node under analysis. One can thus obtain better approximations of the store or detect causal dependencies among the data sent by sensors and the actions carried out by actuators, as well as casuality among nodes.

Conclusions

This paper is a first step towards a formal design framework for IoT, which will support the definition of techniques and tools for certifying properties of IoT applications. We proposed the process calculus IoT-LySa, with primitive constructs to describe the activity of sensors and of actuators, and suitable primitives for managing the coordination and communication capabilities of smart objects. We equipped our calculus with a CFA that statically predicts the interactions among nodes, how data spread from sensors to the network, and how data are put together. We sketched how the result of the analysis can be exploited as the basis for checking and certifying various properties of IoT systems.

Besides the extensions mentioned at the end of Sect. 4, we plan to accurately investigate the exact complexity of the analysis and to implement it. We intend to address with our analysis security and privacy "since IoT deals not only with huge amount of sensitive data (personal data, business data, etc.) but also has the power of influencing the physical environment with its control abilities" [START_REF]IERC: The Internet of Things 2012 -New Horizons[END_REF]. In particular, we can assign specific confidentiality levels to sensors and nodes and by inspecting the result of the analysis, we can detect if nodes with a lower level can access data of entities with a higher level. Also, we will enrich our design framework with security policies, e.g. for access control. By tracking the actions of actuators as suggested in Sect. 4, one can predict if an actuator is maliciously triggered by an attacker, as happened in the recent attack performed through a vehicular infotainment network (http://www.wired.com/2015/07/ hackers-remotely-kill-jeep-highway/). For brevity, we neglected here the cryptographic primitives LySa offers natively, although both the current operational semantics and the static analysis can easily be extended to cover them. An analysis that identifies where encryption and decryption are really needed would be very useful for designers of IoT systems, because cryptography is expensive since many smart devices have limited battery power. Beneficial to such an analysis may be the preliminary work on an enhanced version of IoT-LySa [START_REF] Bodei | Securing IoT communications: at what cost?[END_REF] that estimates costs of cryptographic primitives. Finally, in the IERC words: "there is still a lack of research on how to adapt and tailor existing research on autonomic computing to the specific characteristics of IoT" [START_REF]IERC: The Internet of Things 2012 -New Horizons[END_REF]. To contribute to these issues, we plan to extend our calculus with linguistic mechanisms and a verification machinery to deal with adaptivity in the style of [START_REF] Degano | A Two-Component Language for Adaptation: Design, Semantics, and Program Analysis[END_REF].

To the best of our knowledge, only a limited number of papers addressed the specification and verification of IoT systems from a process calculi perspective, within the formal methods approach. The IoT-calculus [START_REF] Lanese | Internet of things: a process calculus approach[END_REF] is one of the first proposals in this setting. It explicitly includes sensors and actuators, and smart objects are represented as point-to-point communicating nodes of heterogeneous networks. Differently from ours, their interconnection topology can vary at run time. The authors propose two notions of bisimilarity that capture system behaviour from the point of view of end-users and of the other devices. The timed process calculus CIoT [START_REF] Castiglioni | A semantic theory for the internet of things[END_REF] specifies physical and logical components, addresses both timing and topology constraints, and allows for node mobility. Furthermore, communications are either short-range or internet-based. The focus of this paper is mainly on an extensional semantics that provides a fully abstract characterisation of the proposed contextual equivalence.

Many design choices of the above-discussed proposals are similar to ours. The main difference is that our coordination model is based on a shared store à la Linda instead of a message-based communication à la π-calculus. Furthermore, differently from [START_REF] Lanese | Internet of things: a process calculus approach[END_REF][START_REF] Castiglioni | A semantic theory for the internet of things[END_REF], we are here mainly interested in developing a design framework that includes a static semantics to support verification techniques and tools for certifying properties of IoT applications.

The calculi above and ours are built upon those previously introduced for wireless, sensor and ad hoc networks ([16,20,18] to cite only a few). In particular, the calculus in [START_REF] Nanz | Static analysis of topology-dependent broadcast networks[END_REF] is designed to model so-called broadcast networks, with a dynamically changing topology. It presents some features very similar to ours: an asynchronous local broadcast modality, while intra-node communication relies on a local tuple space. Also, the analysis of the behaviour of broadcast networks is done by resorting to a multi-step static machinery.

Fig. 1 .

 1 Fig. 1. The organisation of nodes in our street light control system.

  v. S store of v ∈ V (|j, Γ |).A command for actuator j by the i th sensor γ.A triggered action (γ ∈ Γ )

Partially supported by Università di Pisa PRA 2016 64 Project Through the fog.

the application of a k-ary function f to produce the set ϑ. Recall that the special abstract value will end up in ϑ if the depth of the abstract functional term exceeds d, and it represents all the functional terms with nesting greater than d. To do that (i) for each term E i , it finds the sets ϑ i , and (ii) for all k-tuples of values

Moreover, in all the rules for terms, we require that Θ( ) includes all the abstract values included in ϑ. This guarantees that only those values actually used are tracked by Θ, in particular those of sensors.

In the analysis of nodes we focus on which values can flow on the network and which can be assigned to variables. The judgements have the form ( Σ, κ, Θ) |= N and are defined by the rules in Table 3. The rules for the inactive node and for parallel composition are standard. Moreover, the rule for a single node : [B] requires that its component B is analysed, with the further judgment ( Σ, κ, Θ) |= B, where is the label of the enclosing node. The rule connecting actual stores Σ with abstract ones Σ requires the locations of sensors to contain the corresponding abstract values. The rule for sensors is trivial, because we are only interested in who will use their values, and so is that for actuators. The rules for processes are in Table 3, and all require that an estimate is also valid for the immediate sub-processes. The rule for k-ary multi-output (i) finds the sets ϑ i , for each term E i ; and (ii) for all k-tuples of values (v

it checks if they belong to κ( ∈ L), i.e. they can be received by the nodes with labels in L. In the rule for input the terms E 1 , • • • , E j are used for matching values sent on the network. Thus, this rule checks whether (i) these first j terms have acceptable estimates ϑ i ; (ii) the two nodes can communicate (Comp( , )); and whether (iii) for each message ( , v1 , • • • , vj , vj+1 , . . . , vk ) in κ( ) (i.e. in any message predicted to be receivable by the node with label ) the values vj+1 , . . . , vk are included in the estimates for the variables x j+1 , • • • , x k . The rule for assignment requires that all the values v in ϑ, the estimate for E, belong to Σ (x). The rule for µh. P reflects our choice of limiting the depth of function applications: the iterative process is unfolded d times. The remaining rules are as expected.

To show our analysis at work, consider again the example in Sect. 2 and the process P cp = µh.(z := 1).(z := noiseRed(z)). z estimate must include at least the following entries (assuming d = 4):

Indeed, all the following checks must succeed:

is in κ( a ) by (d).

Correctness of the analysis. Our CFA respects the operational semantics. The proof of this fact benefits from an instrumented denotational semantics for expressions, the values of which are pairs v, v . Consequently, the store (Σ i with a ⊥ value) and its updates are accordingly extended (the semantics used in Table 1 is

, the projection on the first component of the instrumented one). Just to give an intuition, we will have

), and the assignment x := E will result in the updated store Σ i {(v, v )/x}, where E evaluates to (v, v ). Clearly, the semantics of Table 1

↓1 , the projection on the first component of the instrumented one. In our example, the assignment z := noiseRed(z) of the process P cp stores the pair (v, noiseRed cp (1 cp )) made of the actual value v and of its abstract counterpart.

Since the analysis only considers the second component of the extended store, it is immediate defining when the concrete and the abstract stores agree:

The following theorems establish the correctness of our CFA and the existence of a minimal estimate. Their proofs have the usual schema.

Theorem 1 (Subject reduction).

Theorem 2 (Existence of estimates).

Given N , its estimates form a Moore family that has a minimal element.

The following corollary of subject reduction justifies the title of this paper: we do track the ingredients of IoT data. The first item makes it evident that our analysis determines whether the value of a term may indeed be used along the computations of a system, and clarifies the role of the component Θ; the second item guarantees that κ predicts all the possible inter-node communications. Extending the analysis For simplicity, above we have presented a CFA that only tracks the ingredients of the data handled by IoT nodes. Now, we sketch a few possible extensions.


Vincenzo Ciancia

Diego Latella

Mieke Massink
email: .massink@cnr.it

On-the-Fly Mean-field Model-checking for Attribute-based Coordination

Keywords: Collective Adaptive Systems, Probabilistic On-the-fly Model-Checking, Mean-Field Approximation, Discrete Time Markov Chains

Typical Collective Adaptive Systems (CAS) consist of a large number of interacting objects that coordinate their activities in a decentralised and often implicit way. The design of such systems is challenging, as it requires scalable analysis tools and methods to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean-Field Approximated Model-checking. The FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individuals in the context of very large populations whose global behaviour is approximated using deterministic limit techniques. Recently, specific modelling languages have been proposed for CAS. A key feature of such languages is the attribute-based interaction paradigm. In this paper we present an attribute-based coordination language as a front-end for FlyFast. Its formal probabilistic semantics is provided and a translation to the original FlyFast language is given and proved correct. Application examples are also provided.

Introduction and Related Work

Collective Adaptive Systems (CAS) consist of a large number of entities with decentralised control and varying degrees of complex autonomous behaviour. CAS are at the core of the envisioned smart cities of the future and encompass systems like smart urban transport and smart grids. The pervasive nature of CAS and thus their impact on society requires the development of reliable rigorous design models as well as a priori analysis techniques of such models-covering all relevant aspects of their behaviour, including quantitative and emergent onesbefore they are put into operation 1 .

Model-checking has been widely recognised as a powerful approach to the automatic verification of concurrent and distributed systems. It consists of an efficient procedure that, given an abstract model of the system, decides whether the model satisfies a logical formula, typically drawn from a temporal logic. Unfortunately, traditional model-checking suffers from the so called state-space explosion problem which hampers scalability of the approach. In particular, its application to very large models, like those typical of CAS, is infeasible. In [START_REF] Latella | On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination[END_REF][START_REF] Latella | On-the-fly fast mean-field model-checking[END_REF] Latella et al. presented a scalable mean-field model-checking procedure for verifying bounded PCTL (Probabilistic Computation Tree Logic) [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF] properties of selected individuals in the context of systems consisting of a large number of similar, but independent, interacting objects; a limited form of global system properties can be treated as well. The procedure can be used with huge population sizes, as typical of analysis techniques based on mean-field approximation; the average behaviour of the population is approximated using a population Discrete Time Markov Chain (DTMC) convergence result [START_REF] Boudec | A generic mean field convergence result for systems of interacting objects[END_REF] and is used for representing the context in which the selected individuals operate (see [START_REF] Boudec | A generic mean field convergence result for systems of interacting objects[END_REF][START_REF] Latella | On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination[END_REF][START_REF] Latella | On-the-fly fast mean-field model-checking[END_REF] for details). The model-checking procedure is implemented in the tool Fly-Fast as an instantiation of a probabilistic on-the-fly model-checker; the latter is parametric on (the semantic model of) the modelling language [START_REF] Latella | On-the-fly Probabilistic Model Checking[END_REF][START_REF] Latella | On-the-fly fast mean-field model-checking[END_REF].

FlyFast comes with simple modelling language. An agent2 is a finite state process, a generic state C of which is specified by a state defining equation like C := a 1 .C 1 + . . . + a r .C r . Intuitively, the above notation defines state C of the agent and postulates that there are r outgoing transitions from C,with action a j labelling a transition going from C to C j . A probability value is assigned to each action a by means of a probability function definition a :: E, where the actual probability is given by the value of expression E in the current occupancy measure vector m. Assume a system is composed of N instances of the agent and that the states of the agent are C 1 , . . . C S . The occupancy measure vector at the current time is the vector (m 1 , . . . , m S ) s.t. m j yields the fraction of agents currently in state C j over the total number N of agents. A system specification is a triple composed by an agent specification-given as a set of state defining equations-a set of probability function definitions, and an initial global state. Finally, FlyFast provides the user with formula declarations which allow for the interpretation of bounded PCTL atomic propositions in the model at hand. The computational model is clock-synchronous; at each step each agent must perform an independent step (which may be an idle self-loop) so that the global state probabilities are given as the product of agent step probabilities, and a new occupancy measure vector can be computed. The global system behaviour is thus a DTMC as well as the stochastic process given by the occupancy measure vector. Notably, for N sufficiently large, the latter can be approximated deterministically, i.e. by a function of time. This brings to a dramatic decrease in size of the global state space: at each step, the total number of potential next states drops from S N to S, which makes bounded PCTL model-checking of very large population systems possible (the interested reader is referred to [START_REF] Latella | On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination[END_REF][START_REF] Latella | On-the-fly fast mean-field model-checking[END_REF][START_REF] Boudec | A generic mean field convergence result for systems of interacting objects[END_REF] for details).

Recently, modelling and programming languages have been proposed specifically for autonomic computing systems and CAS [START_REF] De Nicola | The SCEL language: Design, implementation, verification[END_REF][START_REF] Bortolussi | CARMA: collective adaptive resource-sharing markovian agents[END_REF][START_REF] Hillston | Specification and analysis of open-ended systems with Carma[END_REF]. Typically, in such frameworks, a system is composed of a set of independent components where a component is a process equipped with a set of attributes describing features of the component. A classical example of attribute is the component location.

An additional environment is often used for the specification of common or global features. The attributes of a component can be updated during its execution so that the association between attribute names and attribute values is mantained in the dynamic store of the component. Attributes can be used in predicates appearing in language constructs for component interaction. For instance a component may broadcast a message to all those components satisfying a given predicate; similarly a component may wait for a message from any of those components satisfying a given predicate.

In the present paper, we propose an extension of the FlyFast front-end modelling language for dealing with components and predicate-based interaction. The extension has been inspired by Carma [START_REF] Bortolussi | CARMA: collective adaptive resource-sharing markovian agents[END_REF]. Components are expressed as pairs process-store; actions are predicate based multi-cast output and input primitives 3 . Associated to each action there is also an (atomic) probabilistic store-update. For instance, assume components have an attribute named loc which takes values in the set of points of a space type. The following action models a multi-cast via channel α to all components in the same location as the sender, making it change location randomly: α * [loc = my.loc] {loc ← randomLoc(loc)}. Here randomLoc is assumed to be a random generator of points in the space 4 . The computational model is clock-synchronous as well, but at the component level. In addition, each component is equipped with a local outbox. The effect of an output action α * [π r ] σ is to deliver output label α to the local outbox, together with the predicate π r , which receiver components will be required to satisfy, as well as the current store γ of the component executing the action; the current store is updated according to update σ. Note that output actions are non-blocking and that successive output actions of the same component rewrite its outbox. An input action α * [π s ]()σ by a component will be executed with a probability which is proportional to the fraction of all those components whose outboxes currently contain the label α , a predicate π r which is satisfied by the component, and a store γ which satisfies in turn predicate π s . If such a fraction is zero, then the input action will not take place (input is blocking), otherwise the action takes place, the store of the component is updated via σ, and its outbox cleared. Thus, as in the original FlyFast language, component interaction is probabilistic, but now the fraction of the components satisfying the relevant predicates plays a role in the computation of transition probabilities. We provide the formal probabilistic semantics of the extended language and a translation to the original FlyFast language which makes the model-checker support the extended language. The translation is proved correct.

Related Work. As we mentioned before, this work has been inspired by Carma [START_REF] Bortolussi | CARMA: collective adaptive resource-sharing markovian agents[END_REF], which in turn shares features with SCEL [START_REF] De Nicola | The SCEL language: Design, implementation, verification[END_REF]. There are several aspects of either languages that are not present in our proposal. The main reason for the absence of most of them is the fact that this work is intended as a proof of concept rather than the realisation of a ready-to-use tool for reasoning about CAS. So we aim at keeping the language minimal and focussing only on attribute-based interaction in the context of stochastic and mean-field semantics and modelchecking. A feature of Carma not considered here is the notion of global environment, since it represents a singularity point that does not fit well with limit approximation techniques. Finally, we point out that the stochastic semantics of Carma are based on time inhomogeneous CTMCs, due to the fact that action parameters may be time dependent, while we use DTMCs as semantic basis. The notion of the outbox is reminiscent of the notion of the ether in PALOMA [START_REF] Feng | PALOMA: A process algebra for located markovian agents[END_REF] in the sense that the collection of all outboxes together can be though of as a kind of ether; but such a collection is intrinsically distributed among the components so that it cannot represent a bottleneck in the execution of the system neither a singularity point in the deterministic approximation. Fluid model-checking for continuous time systems is addressed in [START_REF] Bortolussi | Fluid model checking[END_REF] where a global model-checking procedure for the Continuous Stochastic Logic (CSL, [START_REF] Baier | Model-Checking Algorithms for Continuous-Time Markov Chains[END_REF]) is given, which is based on continuous limit approximated semantics. Fluid semantics have proved very useful for reasoning about large coordination systems (see e.g. [START_REF] Massink | Fluid Analysis of Foraging Ants[END_REF][START_REF] Bortolussi | Stochastic Process Algebra and Stability Analysis of Collective Systems[END_REF][START_REF] Latella | Investigating Fluid-Flow Semantics of Asynchronous Tuple-Based Process Languages for Collective Adaptive Systems[END_REF]). Predicate-/attribute-based inter-process communication has been originally proposed in [START_REF] Latella | Comunicazione basata su proprietà nei sistemi decentralizzati [Property-based inter-process communication in decentralized systems[END_REF] where several variants of predicate-/attributebased communication primitives-including blocking / non-blocking, bounded / unbounded-are discussed in the context of a study on high-level language constructs for distributed systems with decentralised control (see for instance [START_REF] Lesser | Functionally accurate, cooperative distributed systems[END_REF]). The notion of predicate-/attribute-based interaction is central in the definition of SCEL [START_REF] De Nicola | The SCEL language: Design, implementation, verification[END_REF] where its synchronous-communication variant has been given formal semantics. Asynchronous-communication variants have been defined for stochastic versions of SCEL [START_REF] Latella | On stocs: A stochastic extension of SCEL. Software, Services, and Systems -Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering[END_REF]. An attribute-interaction based calculus is proposed in [START_REF] Alrahman | A calculus for attribute-based communication[END_REF] where broadcast communication links among components are dynamically established on the basis of the interdependences determined by predicates over attributes. A reduction semantics approach is adopted where each transition involves the group composed of both sender and receivers. Attribute π-Calculus has been proposed in [START_REF] John | The attributed pi calculus[END_REF] and extended to Imperative π-Calculus in [START_REF] John | Dynamic compartments in the imperative pi-calculus[END_REF]; in both calculi, which inherit the classical point-to-point communication paradigm of the π-Calculus, as opposed to multi-cast, attributes are related to messages rather than to processes. None of the above mentioned works on predicate-/attributebased languages addresses mean-field approximated model-checking so, to the best of our knowledge, the present paper is the first proposal on the subject.

Attribute-based Coordination Language and Logic

In this section we define an attribute-based population description language and related logic. A system is defined as a population of N identical interacting components 5 in a clock-synchronous fashion. Each component is equipped with a finite set of attributes; the current store γ ∈ Γ of the component maps each attribute name to an attribute value.

Syntax

A component specification is a pair (∆, F ) where ∆ is a finite set of state-defining equations, one for each state of the component and F is a set of auxiliary function definitions 6 . We let S, ranged over by C, C , C 1 , . . . denote the (denumerable, non-empty) set of all states which can be used in equations. Each equation defines the transitions from the state to other states of the component; each transition is labelled by the action the component performs when the transition takes place. The general format of a state defining equation is:

C := [g 1 ]P 1 + . . . + [g r ]P r
where each guard [g] is a predicate π defined according to the following grammar:

π ::= | ⊥ | e 1 e 2 | ¬π | π 1 ∧ π 2 .
(⊥, resp.) stands for the truth value true (false resp.), while ∈ {≥, >, ≤, <}; we let ∈ {>, <}. An expression e can be an attribute name a, or my.a referring to the value of a in the component where it occurs, or a value v in given set V. In defining equations as above, we abbreviate [ ]P j with P j and we omit summands of the form [⊥]P j . Each P j in a state defining equation as above is of the form p j :: act j .C j , where p j is a probability expression, i.e. an expression with value in [0, 1], built from constants v ∈ [0, 1] and the special operator frc C, combined using standard arithmetic operators; for state C, frc C returns the fraction of the components that are currently in state C, over the total of N components. Clearly, the use of the frc operator allows action (and, ultimately, transition) probability to depend on the global state of the system. Actions act j can be output actions α * [π] σ or input actions α * [π]()σ. We assume a countable set of action types A, with α ∈ A. The effect of an output action α * [π] σ is a broadcast to all those components satisfying predicate π and which are willing to accept the interaction. This is achieved by means of delivering α , together with some additional information, to the outbox of the component executing the action, as we will discuss in detail in Sect. 2.2. In addition, the store of the component executing the action is updated according to the update σ, which is a function from Γ to the class of probability distributions over Γ -i.e., in the general case, the update may be probabilistic. Similarly, an input action α * [π]()σ is used to receive an α-message sent by a component satisfying predicate π. More specifically, the probability of executing the input action will be proportional to the fraction of components which have sent the α-message while satisfying predicate π and requiring a predicate which is satisfied by the component executing the input action. Also input actions are provided with a store update σ whereas the component outbox is cleared as (a side) effect of their execution. In the sequel, we shall call address predicates the predicates [π] used for identifying the partners in input/output actions. For updates, we use in a given set being unreachable from states of other sets. Each such a set of states can be seen as a component with a different behaviour.

the following notation: {a 1 ← e γ 1 , . . . , a t ← e γ t } where e γ j is an expression which may also include functions-the definition of which are to be provided in Fwhich may depend on the component store γ and produce random results, as we shall see below. Attributes different from a 1 , . . . , a t are left unchanged by the update. We require that any attribute name a occurring in a guard [g], or in the expressions e γ 1 , . . . , e γ t , must appear in the form my.a (thus referring to the value of the attribute in the local store of the component). An attribute name a may appear both with and without the my. prefix in the address predicate π. Intuitively, equation C := [g 1 ]P 1 + . . . + [g r ]P r defines state C of the component at hand and postulates that there are r potential outgoing transitions from C, with action act j labelling a transition going from C to C j . The actual transitions will be determined by the value of the guards and the action probabilities. Note that it may happen that the current cumulative probability value of the enabled transitions is less than 1; for this reason, the language provides the construct rest :: α[π] σ.C, where rest is defined as the residual probability; it is required that there is at most one rest-branch (typically the last one) in every state defining equation. Only output actions are allowed in rest-branches; this ensures that the residual probability is not affected by the fraction of those components in the system satisfying the address predicate. Obviously, in a given component specification there is exactly one defining equation for each state of the component. We let S ∆ denote the finite set of states defined by ∆. Similarly, Γ ∆ , A ∆ and Π ∆ denote the set of all stores associated to ∆, the action types and the predicates occurring in (the equations of) ∆. Finally, we let V ∆ denote the set of values which can be taken by the attributes of a component specified by ∆. Note that we assume V ∆ is a finite set-thus also Γ ∆ is finite; model finiteness is a common assumption for modelling languages supported by automatic analysis and verification tools.

Example 1 (A spatially distributed Computer Epidemic Model). We enrich the Computer Epidemic Model of [START_REF] Bortolussi | Continuous approximation of collective systems behaviour: A Tutorial[END_REF], SEIR, with infection communication and a bi-dimen-sional Regular GRID [START_REF] Ciancia | On Space in CARMA[END_REF] model for space, where for each point the following specific operators are defined, with the usual North, South, East, West meaning: N( ), S( ), E( ), W( ). Each component is equipped with a position attribute, named loc, which is always yielding the current position (i.e. point) in space of the component and is the only attribute of the component. Note that, given the abstract nature of the bi-dimensional Regular GRID, such a "point" could be a physical point is space, but also a specific region (or patch) in a patched representation of space. We will implicitly refer to the second interpretation in the sequel. In the model, given in Fig. 1, the purpose of auxiliary function Jump is twofold: (i) it defines a function from positions to discrete probability distributions which, given position , characterizes a probability distribution which assignes probability p N ( ) to N( ), probability p S ( ) to S( ), and so on and (ii) defines a random position generator which, given position , randomly returns a new position according to the specified probabilities. Note that the probabilities are themselves functions of the position and they are assumed being declared as additional auxiliary functions. In the equation for S in Fig. 1 probability constants h, m N , . . . , m W are factors in [0, 1] with cumulative value at most 1, each to be multiplied by the actual probability of the associated (input) action. The latter will be computed as the fraction of the local states which satisfy the required predicate. The resulting values, when taken all together, will characterize a probability sub-distribution; the residual probability will be associated to a rest-self-loop. Similar considerations apply to the probability constants in the definition of other states (e.g. i in the figure). We assume

h > m N ≈ m S ≈ m E ≈ m W .
In other words, an agent has higher probability to get the infection from agents in the same place than from agents in adjacent places; the probability drops to zero in all other cases. •

A system is modelled as a population of N instances of a component, so a system specification Υ is a triple (∆, F, Σ 0 ) (N ) where (∆, F ) is a component specification and Σ 0 is the initial (system) global state, which will be discussed below. In the sequel we will often write ∆ instead of (∆, F ).

Probabilistic Semantics

In order to model component interactions within a system, each component is equipped with a local outbox. The idea is that, whenever a component executes an output action, the related output will be available in the component's outbox only during the next clock tick; in the next state, (other) components will be able to get the message by means of corresponding input actions. After such a tick, the outbox will be empty or filled with the information generated by a subsequent output action of the component. Formally, let Λ O ∆ be the set

Λ O ∆ = {α |α ∈ A ∆ }. An outbox-state O ∈ O ∆ = { } ∪ (Γ ∆ × Π ∆ × Λ O ∆ ) is either empty or a triple (γ, π, α ). A component-state Σ is a triple Σ = (C, γ, O) ∈ S ∆ × Γ ∆ × O ∆ = Ω ∆ ,
= ((C 1 , γ 1 , O 1 ), . . . , (C N , γ N , O N )) ∈ Ω N ∆ where Σ [j] = (C j , γ j , O j )
is the component-state of the j-th instance in the population for j = 1 . . . N . We say that N is the population size of the system. In the sequel, we will omit the explicit indication of the size N in (∆, F, Σ 0 ) (N ) , and elements thereof or related functions, writing simply (∆, F, Σ 0 ), when this cannot cause confusion. In summary, a system specification can be thought of as process algebraic clock-synchronous parallel composition of N processes. The probabilistic behaviour of a system can be derived from its specification (∆, F, Σ 0 ) (N ) . We remind that Ω ∆ is finite, since so are sets S ∆ , Γ ∆ and O ∆ . Assume Ω ∆ = {Σ 1 , . . . , Σ S } and let U S be the set {m ∈ [0, 1] S | S i=1 m [i] = 1}; we can assume, w.l.o.g. that there is a total ordering on Ω ∆ so that we can unambiguously associate each component m j of a vector m = (m 1 , . . . , m S ) ∈ U S with a distinct element Σ j of {Σ 1 , . . . , Σ S }. With each global state Σ (N ) an occupancy measure vector M (N ) (Σ (N ) ) ∈ U S is associated where

M (N ) (Σ (N ) ) = (M (N ) 1 , . . . , M (N ) S ) with M (N ) i = 1 N N n=1 1 {Σ (N )
[n] =Σi} for i = 1, . . . , S and the value of 1 {α=β} is 1, if α = β, and 0 otherwise. So, for

Σ i = (C i , γ i , O i ), M (
E L [[a]] γ = a, E L [[my.a]] γ = γ(a), E R [[a]] γ = γ(a), and E P [[frc C]] m = S i=1 {m [i] |Σ i = (C, γ i , O i )}; moreover, E R [[my.a]] γ , E P [[tt]] m , E P [[ff]] m , E L [[frc C]] γ , and E R [[frc C]
] γ are undefined as are, for the sake of simplicity, E P [[a]] m , E P [[my.a]] m . The definition of the above semantic interpretation functions on composition terms can be given recursively on the structure of the terms and is left out here. In particular, we assume them extended to tuples. Similarly, we assume standard techniques and machinery for auxiliary functions in store updates; the semantics of update σ in the current store γ will be denoted by E U [[σ]] γ , that is a probability distribution over stores 7 .

Let Λ ∆ be defined as

Λ ∆ = Λ O ∆ ∪ Λ I ∆ ,
→ ⊆ Ω ∆ × Θ ∆ × Ω ∆ such that (C, γ, O) λ,p ---→ (C , γ , O ) iff C := j∈J [g j ]p j :: act j .C j is the defining equation for C and p = k∈J {p k |(C, γ, O) λ, pk ----→ k (C , γ , O )}
, where λ, pk ----→ k is the least relation induced by the rules in Fig. 2. The component transition matrix function

C := j∈J [gj]pj :: actj.Cj k ∈ J E L [[g k ]]γ = tt act k = α * [π] σ p = E U [[σ]]γ(γ ) (C, γ, O) α ,p•E P [[p k ]]m -----------→ k (C k , γ , (γ, E L [[π]]γ, α )) (1)
C := j∈J [gj]pj :: actj.Cj k ∈ J [g k ]p k = rest act k = α * [π] σ p = E U [[σ]]γ(γ ) (C, γ, O) α ,p•(1-j∈(J\{k}) E P [[p j ]]m) ----------------------→ k (C k , γ , (γ, E L [[π]]γ, α )) (2)
C := j∈J [gj]pj :: actj.Cj k ∈ J E L [[g k ]] = tt act k = α * [π]()σ p = E U [[σ]]γ(γ ) f = S i=1 {m [i] |Σi = (C i , γ i , (γ i , π i , α )) ∧ E R [[π i ]]γ = E R [[E L [[π]]γ]] γ i = tt} (C, γ, O) α(),p•E P [[p k ]]m•f ------------→ k (C k , γ , ) (3)
Fig. 2. Probabilistic Semantics Rules K (N ) (m) Σ,Σ is defined as follows: K (N ) (m) Σ,Σ = (λ,p)∈Θ ∆ {p|Σ λ,p ---→ Σ }. Note that all the above summations are finite under our assumption that so is V ∆ . The behaviour of the system is the result of the parallel-synchronous execution of the N instances of the component. Thus, the probabilistic behaviour of the system is characterised by the DTMC X (N ) (t) with initial probability distribution δ Σ0 and one step probability matrix P (N ) defined by the following product:

P (N ) Σ,Σ = Π N n=1 K (N ) (M (N ) (Σ)) Σ [n] ,Σ [n] .
Of course, the 'occupancy measure' view of the evolution in time of stochastic process X (N ) (t) is again a DTMC, namely the occupancy measure DTMC, which is defined as expected:

M (N ) (t) = M (N ) (X (N ) (t)).

Bounded PCTL

We recall that, given a set P of atomic propositions, the syntax of PCTL state formulas Φ and path formulas ϕ is defined as follows, where ap ∈ P and k ≥ 0:

Φ ::= ap | ¬ Φ | Φ ∧ Φ | P p (ϕ)

A Translation to FlyFast

In this section we define a translation I such that, given system specification Υ = (∆ Υ , F Υ , Σ 0 ) (N ) , I(Υ ) = ∆, A, C 0 (N ) is a FlyFast [START_REF] Latella | On-the-fly fast mean-field model-checking[END_REF][START_REF] Latella | On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination[END_REF] system specification preserving probabilistic semantics. The attribute-based FlyFast front-end is then completed with a simple translation at the PCTL level, also provided in this section. We map every component state of Υ to a distinct state of I(Υ ) by means of a total injection I S : Ω ∆ Υ → S. The mapping of actions is a bit more delicate because we have to respect FlyFast static constraints and, in particular, we have to avoid multiple probability function definitions for the same action. To that purpose, we could distinguish different occurrences of the same action in different transitions, characterized by their source and target states in Ω ∆ Υ . In practice, since an action of a component cannot be influenced by the current outbox of the component, it is sufficient to use a total injection I A of the following type (S ∆ Υ ×Γ ∆ Υ )×Λ ∆ Υ ×Ω ∆ Υ → A for the mapping of actions. In the sequel we show how to build

I(Υ ) = ∆, A, C 0 (N ) from Υ = (∆ Υ , F Υ , Σ 0 ) (N )
. The translation algorithm is given in Fig. 3, where for action act ∈ {α * [π] σ, α * [π]()σ} we let T (act) = α, P (act) = π, and U (act) = σ. SUM{t|cond(t)} denotes the syntactical term representing the sum of terms t ∈ {t|cond(t) = tt}, i.e. t 1 + . . . + t n , if {t|cond(t) = tt} = {t 1 , . . . , t n } = ∅ and 0 if {t|cond(t) = tt} is the empty set. Finally, by t * t we mean the syntactical term representing the product of terms t and t . Output actions are dealt with in step 1. Consider for example action For each state equation C := j∈J [gj]pj :: actj.Cj in ∆Υ :

1. For each output action α * [π] σ = act k with k ∈ J, and γ ∈ Γ∆ Υ , let Jα,σ,γ be the largest subset of J s.t. there is C ∈ S∆ s.t. for all j ∈ Jα,σ,γ Cj = C ,

T (actj) = α, E L [[P (actj)]]γ = E L [[π]]γ, and E U [[U (actj)]]γ = E U [[σ]]γ. For each γ ∈ Γ∆ Υ , with ξ = IA ((C, γ), α , (C , γ , (γ, E L [[π]]γ, α ))
), the following action probability function definition is included in A: ξ ::

E U [[σ]]γ(γ ) * SUM{pj|j ∈ Ĵα,σ,
= C , T (actj) = α and E U [[U (actj)]]γ = E U [[σ]]γ.
For each γ ∈ Γ∆ Υ , with ξ = IA ((C, γ), α(), (C , γ , )), the following action probability function definition is included in A: ξ :: Since the action is not depending on the current outbox, in practice a copy of such a transition is generated for each component state sharing the same proper state S and the same store γ. In the general case, in a defining equation for a state C there might be multiple occurrences of the same action, bringing to the same next state C ; the algorithm takes care of this and collects them in order to generate a single transition; the appropriate probability is expressed by means of the SUM{. . .} term. The translation scheme for input actions is defined in case 2 and is similar, except that for each term p j in the SUM{. . .} expression one has also to consider the sum Φ j of the fractions of the possible partners. The translation of the rest case is straighforward. Let K

E U [[σ]]γ(γ ) * SUM{(pj * Φj)|j ∈ Ĵα,σ,γ}, where Ĵα,σ,γ = {j ∈ Jα,σ,γ|[gj]pj = rest ∧ E L [[gj]]γ = tt} and term Φj is: SUM{frc IS (( C, γ, (γ, π, α )))|E R [[π]]γ = E R [[E L [[πj]]γ]]γ = tt}. Moreover, for each outbox O ∈ O∆ Υ ,
(N )

I(Υ ) : U S × I S (Ω ∆ ) × I S (Ω ∆ ) → [0, 1
] be the step probability function associated to I(Υ ) by the FlyFast language probabilistic semantics definition (see [START_REF] Latella | On-the-fly fast mean-field model-checking[END_REF][START_REF] Latella | On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination[END_REF] for details) and

K (N ) Υ : U S × Ω ∆ × Ω ∆ → [0, 1]
be the step probability function for Υ as defined in Sect. 2.2. It is easy to see that: Theorem 1. For all N > 0, occupancy measure vector m ∈ U S and Σ, Σ ∈ Ω ∆ the following holds:

K (N ) Υ (m) Σ,Σ = K (N ) I(Υ ) (m) I S (Σ),I S (Σ ) .
Proof (scketch). We first observe that, by definition,

K (N ) Υ (m) (C,γ,O),(C ,γ ,O ) = (λ,p)∈Θ ∆ {p|(C, γ, O) λ,p ---→ (C , γ , O )} which, by definition of -→ , is equal to (λ,p)∈Θ ∆ {p|p = k∈J {p k |(C, γ, O) λ, pk ----→ k (C , γ , O )} ∧ C := j∈J [g j ]p j :: act j .C j is the def. eq. of C in Υ }.
Consider the outer summation and suppose (α , p) be the index of a summand. Without loss of generality, assume there is only one instance of such a summand and there is only one k ∈ J such that the following transition is derived using the rules of Fig. 2 [START_REF] Latella | On-the-fly fast mean-field model-checking[END_REF][START_REF] Latella | On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination[END_REF], we get that the probability assigned to

ξ is E U [[σ]] γ (γ )• E P [[p k ]] m , that is, exactly pk . Thus K (N ) Υ (m) Σ,Σ = K (N ) I(Υ ) (m) I S (Σ),I S (Σ ) .
The proof for all the other cases is similar.

•

The translation of atomic proposition declarations into FlyFast formula declarations is the obvious one and is shown in

Epidemic Example Revisited

We return to the distributed Epidemic example of Fig. 1 where, for the sake of simplicity, we consider a simple patched space, consisting of the usual four quadrants A, B, C, D in the Cartesian Plane, as in Fig. 5 (left). We model a 'flow' from quadrant C to quadrant A by defining the jump probabilities as in the table in Fig. 5 (right) 9 , where l = 0.6 and s = 1 -l, so that l > s. Fig. 6 shows the fast-simulation results10 for the model for each of the four quadrants. This functionality is built-in in the FlyFast tool. In the figure, the fractions of numbers of the components in each of the four states at each of the four locations are shown. Note that these fractions correspond to appropriate predicates on standard atomic propositions; for instance the fraction of components in state S at quandrant A is captured by s ∧ a, assuming the following declarations: s at S and a def (my.loc = A). The simulation of single elements, taken as the average over 10 runs shows a very good correspondence with the fast-simulation results. The results also show good correspondence to the original SEIR model [START_REF] Bortolussi | Continuous approximation of collective systems behaviour: A Tutorial[END_REF] when the probability to move between quadrants is set to zero and in the initial state the total population is in state S and in one specific quadrant in the former model. Besides fast simulation, that gives an idea of the average global behaviour of the system, we can also analyse the behaviour of a single component in the context of the overall behaviour. We consider two example properties as illustration. Let us first consider a component initially in state S and located in A and let atomic propositions i and c be declared as follows: i at I and c def (my.loc = C). The following formula (P1) states that the probability is greater than p that that the component ends up infected in quadrant C by time t: P >p (tt U ≤t (i ∧ c)). FlyFast allows one to study the dynamics of the actual probability as a function of t, by means of the notation P =? (tt U ≤t (i ∧ c)) and the resulting graph, for the above initial conditions and for the first 70 time units is shown in Fig. 7 (left). For comparison, the formula for an agent starting in C and ending up in A and being infected is shown as well in the same figure. The results for a more complicated, nested, formula (P2) are shown in Fig. 7 (right). P2 expresses the probability, over time, of a component reaching a situation in which it is neither infected nor exposed, and from which it can reach a state in which it has a probability higher than 0.15 to be infected and located in C within the next 10 time units; formula P2 is given below, where i is assumed defined by i at I: P =? (tt U ≤t (¬(i ∨ e) ∧ P >0.15 (tt U ≤10 (i ∧ c)))). The formula has been considered for a component which is initially in A and in state S; the figure shows also a similar formula, where the role of A and C is exchanged and a probability higher than 0.45 instead of 0.15 is considered. For both types of properties a considerable difference in the probabilities can be observed for an agent that is initially located in A or in C, due to the flow of movement that has been introduced. This illustrates a clear dependence of the results on the dynamically changing spatial distribution of components. The total number of states, actions and transitions for the resulting FlyFast object specification is 52, 114 and 468 respectively, while the number of states of the global approximated model which have been generated for the analysis of formula P2 is 2.323 (2.185 when A and C are swapped). The model checking time for the more complicated nested formula P2 and for all values of t (70) is 10.343 (9.921 when A and C are swapped) ms, ≈ 148 (141) ms per checking session, for a model with a total population of 10.100 objects. A well-known feature of mean-field model checking is that the model checking time is independent of the size of the population, however, further experimentation with more extended spatial models and more attributes, that do effect this time, is planned as future work.

A B C D pH pN pS pE pW A l 0 s/2 0 s/2 B s/2 0 s/2 l 0 C s l/2 0 l/2 0 D s/2 l 0 0 s/2

Conclusions

The attribute-based interaction paradigm is deemed fundamental for agent interaction in the context of Autonomic or Collective Adaptive Systems [START_REF] De Nicola | The SCEL language: Design, implementation, verification[END_REF][START_REF] Latella | On stocs: A stochastic extension of SCEL. Software, Services, and Systems -Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering[END_REF][START_REF] Bortolussi | CARMA: collective adaptive resource-sharing markovian agents[END_REF][START_REF] Alrahman | A calculus for attribute-based communication[END_REF][START_REF] Hillston | Specification and analysis of open-ended systems with Carma[END_REF]. In this paper we have presented a attribute-based coordination modelling language as a front-end for FlyFast, an on-the-fly mean-field model-checker for bounded PCTL. The language extends the original FlyFast modelling language by replacing its actions with input (output, respectively) actions where senders (receivers, respectively) are specified by means of predicates on dynamic attributes on system components, where a component is a process/attribute-store pair. A translation to the standard FlyFast language has been presented, its correctness has been showed as well as an example of its application to a simple case study. It should be noted that the introduction of attributes in a process model is an intrinsic source of complexity in terms of component state-space size. Such an increase, in the worst case, goes with

|V ∆ | |Att ∆ | • (|A O ∆ | + 1)
, where Att ∆ is the set of attributes of the component, V ∆ is the set of values they can take, and A O ∆ is the set of output actions occurring in the component specification (which may appear in its outbox). The obvious consequence of this is that one has to carefully ponder the importance and necessity of each and every new attribute used in a model, although, it must be kept in mind that the real source of state-space explosion is the size of the system, and this issue is addressed by Mean-Field approximation. A first optimisation consists in considering only reachable component states as well as eliminating actions with constant zero probability and simplifying boolean combinations of FlyFast atomic propositions in the translation. A possible additional line of investigation is the study of techniques for DTMC minimization to Mean-field analysis, so that the number of difference equations can decrease as a consequence, in a similar way as for CTMCs and the number of differential equations in fluid flow analysis [START_REF] Tschaikowski | A unified framework for differential aggregations in markovian process algebra[END_REF].

,Fig. 1 .

 1 Fig. 1. A four state model: susceptible (S), exposed (E), infected (I), and recover (R).

  where C, γ, O are the current state, store and outboxstate of the component, respectively. If the component-state is the target of a transition modelling the execution of an output action, then O = (γ , π, α ), where γ is the store of the (component-state) source of the transition, π is the predicate used in the action-actualized with γ -and α the actual message sent by the action. If, instead, the component-state is the target of a transition for an input action, then O = , i.e. the empty outbox. A global state is a tuple Σ

  N ) i is the fraction, in the current global state Σ (N ) , of the component instances which are in state C i , have store γ i and outbox O i , over the total number N . We assume semantic interpretation functions E L [[•]] and E R [[•]] for the local, remote respectively, interpretation of expressions and predicates and a function E P [[•]] for the interpretation of probability expressions. E L [[e]] (E R [[e]], respectively) takes a local (remote, respectively) store γ as an argument, whereas E P [[p]] takes an occupancy measure vector m as an argument. We note that

  with Λ O ∆ as above, and Λ I ∆ = {α()|α ∈ A ∆ }. A component specification (∆, F ) characterises the (component) transition probability matrix as a function of occupancy measure vectors m, K(N ) : U S × Ω ∆ × Ω ∆ → [0, 1] such that K (N ) (m) Σ,Σ is the probability of a one step jump from component-state Σ to component-state Σ , given (that the global system state induces) occupancy measure vector m. K (N ) (m) Σ,Σ is computed by making use of a transition relation (C, γ, O) λ,p ---→ (C , γ , O ) over the space of component-states Ω ∆ , with transition labels drawn from Θ ∆ ⊂ Λ ∆ × [0, 1]. More specifically, the transition relation is the relation -

  where ϕ ::= X Φ | Φ U ≤k Φ. PCTL formulas are interpreted over state labelled DTMCs, which are pairs (M, L) where M is a DTMC and L is a mapping from the set of states of M to 2 P ; for each state s, L(s) is the set of atomic propositions true in s 8 . For the purposes of FlyFast bounded PCTL model-checking, our system specifications are enriched with the declaration of three different kinds of atomic propositions. A declaration of the form ap at C associates atomic proposition ap to state C ∈ S ∆ . Thus ap must be included in the set L(Σ) for each global state Σ = ((C 1 , γ 1 , O 1 ), . . . , (C N , γ N , O N )) such that C 1 = C (recall here that FlyFast performs model-checking of the first object in the context of the global system). A declaration of the form ap def (my.a v) associates atomic proposition ap to all component-states (C, γ, O) s.t. attribute a is v. So, ap must be included in the set L(Σ) for each global state Σ = ((C 1 , γ 1 , O 1 ), . . . , (C N , γ N , O N )) such that E L [[my.a v]] γ1 = tt. Finally, a limited form of global atomic predicate is provided by means of a declaration of the form ap def (frc C v); in this case, ap must be included in the set L(Σ) for each global state Σ s.t. the fraction in Σ of the component states (C, γ, O), for any γ and O, is than v ∈ [0, 1].

3 .

 3 the following summand is added to the equation in ∆ for state IS (C, γ, O): ξ. IS (C , γ , ); If there exists k ∈ J s.t. [g k ]p k = rest, and act k = α * [π] σ, let Ā be the set of probability function definitions which has been constructed in steps (1) and (2) above; note that for every ζ :: p * q ∈ Ā, q is either a probability constant pj occurring in a branch [gj]pj :: actj.Cj of the defining equation for C, or it is a term of the form SUM{(p h * Φ h )|h ∈ H}, for some index set H. We define p = (1 -SUM{q|ζ :: p * q ∈ Ā}) and, for all γ ∈ Γ∆ Υ , with ξ = IA ((C, γ), α , (C k , γ , (γ, E L [[π]]γ, α ))), the following action probability function definition is included in A: ξ :: E U [[σ]]γ(γ ) * p. Moreover, for each outbox O ∈ O∆ Υ , the following summand is added to the equation in ∆ for state IS (C, γ, O): ξ. IS (C k , γ , (γ, E L [[π]]γ, α )); 4. No other action probability function definition and transition is included and the initial state C0 of I(Υ ) is defined as C0 = IS (Σ0).

Fig. 3 .

 3 Fig. 3. The translation algorithm

  : (C, γ, O) α , pk -----→ k (C , γ , O ). So, we have K (N ) Υ (m) (C,γ,O),(C ,γ ,O ) = pk such that (C, γ, O) α , pk -----→ k (C , γ , O ), where C := j∈J [g j ]p j :: act j .C j is the defining equation for C. Suppose [g k ]p k = rest, so that Rule (1) of Fig. 2 has been used for generating the transition. Thisimplies that E L [[g k ]] γ = tt, pk = E U [[σ]] γ (γ ) • E P [[p k ]] m , C = C k , and O = (γ, E L [[π]] γ , α ).Under the above conditions, by definition of the translation algorithm, the action ξ = I A ((C, γ), α , (C , γ , O )) and related action probability function definition ξ :: E U [[σ]] γ (γ ) * SUM{p k } are included in the FlyFast model. Moreover, the summand ξ. I S (C , γ , O ) is added in the equation for state I S (C, γ, O) in the FlyFast model. Using the semantics definition of the FlyFast language

Fig. 4 where

 4 OR{e|cond(e)} denotes the syntactical term representing the disjunction of expressions e ∈ {e|cond(e) = tt}, i.e. e 1 | . . . |e n , if {e|cond(e) = tt} = {e 1 , . . . , e n } = ∅ and ff, if {e|cond(e) = tt} is the empty set.

Fig. 4 .

 4 Fig. 4. Translation of atomic proposition declarations. The translation is not defined whenever OR{t|cond(t)} = ff or SUM{t|cond(t)} = 0.

Fig. 5 .

 5 Fig. 5. The Cartesian quadrants (left) and the jump probabilities (right).

Fig. 6 .

 6 Fig. 6. Fast simulation for each of the four quadrants.

Fig. 7 .

 7 Fig. 7. Model checking results for properties P1 (left) and P2 (right).

  γ}, where Ĵα,σ,γ = {j ∈ Jα,σ,γ|[gj]pj = rest ∧ E L [[gj]]γ = tt}. Moreover, for each outbox O ∈ O∆ Υ , the following summand is added to the equation in ∆ for state IS (C, γ, O): ξ. IS (C , γ , (γ, E L [[π]]γ, α )); 2. For each input action α

*

[π]()σ = act k , with k ∈ J, and γ ∈ Γ∆ Υ , let Jα,σ,γ be the largest subset of J s.t. there is C ∈ S∆ s.t. for all j ∈ Jα,σ,γ Cj

In the context of FlyFast we use the words agent, process and object as synonyms.

For the sake of notational simplicity, in this paper we present a non value-passing version of the FlyFast front-end; the complete, value-passing, approach is described in[START_REF] Ciancia | An Attribute-based Front-end for FlyFast[END_REF].

Multi-cast interaction is denoted using the * notation, as in Carma.

In practice, the fact that the components are identical is not a strong limitation since each component may consist of several different sets of states, with each state

The specific syntax of auxiliary function definitions is irrelevant and left out here.

In this paper, for the sake of simplicity, updates do not depend on the current occupancy measure vector, i.e. the frc operator cannot occur in their specification.

We refer to[START_REF] Hansson | A logic for reasoning about time and reliability[END_REF] for the formal definition of PCTL and to[START_REF] Latella | On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination[END_REF][START_REF] Latella | On-the-fly fast mean-field model-checking[END_REF] for the details of its instantiation in FlyFast.

We assume:N(A) = N(B) = S(C) = S(D) = E(A) = E(D) = W(B) = W(C) = undefined, with [loc = undefined] = ⊥ for all loc .

Experiments have been performed using the FlyFast on-the-fly mean field model checker on a PC with an Intel Core i7 1.7GHz, RAM 8Gb.

Research partially funded by the EU project QUANTICOL (nr. 600708).