=Paper=
{{Paper
|id=None
|storemode=property
|title=A Framework to Specify and Verify Computational Fields for Pervasive Computing Systems
|pdfUrl=https://ceur-ws.org/Vol-892/paper2.pdf
|volume=Vol-892
|dblpUrl=https://dblp.org/rec/conf/woa/CasadeiV12
}}
==A Framework to Specify and Verify Computational Fields for Pervasive Computing Systems ==
https://ceur-ws.org/Vol-892/paper2.pdf
A Framework to Specify and Verify Computational
Fields for Pervasive Computing Systems
Matteo Casadei and Mirko Viroli
Alma Mater Studiorum – Università di Bologna, Italy
{m.casadei,mirko.viroli}@unibo.it
Abstract—Pervasive context-aware computing networks call special case of computational field) pumped by the device [2].
for designing algorithms for information propagation and re- Computational fields have been adopted in several pervasive
configuration that promote self-adaptation, namely, which can computing domains, surveyed in [6], to devise efficient and
guarantee – at least to a probabilistic extent – certain reliability
and robustness properties in spite of unpredicted changes and robust algorithms for routing and communication in sensor
conditions. The possibility of formally analyzing their properties networks, provide support for context awareness in mobile
is obviously an essential engineering requirement, calling for pervasive computing applications, and coordinate task assign-
general-purpose models and tools. ment in situated settings. Programming frameworks for com-
As proposed in recent works, several such algorithms can be putational fields include the TOTA middleware [12], the Proto
modeled by the notion of computational field: a dynamically
evolving spatial data structure mapping every node of the language [2], [1], the chemical-oriented models proposed in
network to a data value. Based on this idea, as a contribution [17], [19].
toward formally verifying properties of pervasive computing
systems, in this article we propose a specification language to Despite the dynamic and unpredictable nature intrinsic
model computational fields, and a framework based on PRISM to pervasive computing domains, very little effort has been
stochastic model checker explicitly targeted at supporting tem- devoted so far to define verification techniques able to formally
poral property verification. By a number of pervasive computing analyze probabilistic and temporal properties of their algo-
examples, we show that the proposed approach can be effectively
used for quantitative analysis of systems running on networks rithms, e.g. providing probability of convergence or average
composed of hundreds of nodes. convergence time. In this article we tackle this issue by a
framework for probabilistic model checking of computational
I. I NTRODUCTION fields. We propose a specification language to formally define
The study and adoption of novel distributed approaches to and model such algorithms, and support their stochastic verifi-
computing is getting more and more importance as a result cation via translation into a CTMC (Continuous Time Markov
of the growing trend toward pervasive and mobile computing Chain) model, most specifically, into a specification for the
scenarios [22]. This is leading to developing a new class of well-known PRISM stochastic model checker [8]. In fact,
applications, intrinsically distributed and mobile, ranging from stochastic model checking allows to cope with the probabilistic
providing a better interaction with the physical environment to aspects proper of computational fields and their distributed
managing and improving cooperation among human activities. nature: probability plays a key role in both analyzing the
This picture poses new challenges in the development of unpredictable behaviors typical of open domains – such as
pervasive systems, that cannot be dealt with by traditional pervasive systems – and deriving robust and self-adaptive
centralized approaches. In fact, these emerging domains re- algorithms for pervasive scenarios. State-space explosion is
quire for applications to support: (i) self-adaptivity, i.e. the addressed by relying on approximate results according to the
ability to cope with unpredicated changes like the mobility of approach described in [7]. We discuss our approach by refer-
system actors, locally managing the resulting changes in the ence algorithms useful in pervasive domains, such as gradient
computing environment in an unsupervised way; (ii) context- diffusion, gradient descent, and information segregation.
awareness, i.e. handling spatially situated activities depending The main contribution resulting from this article is a frame-
on the surrounding physical and virtual context. work explicitly targeted at modeling and analyzing computa-
The computational field (or simply field) notion is recog- tional fields through stochastic model checking, demonstrating
nized as a fundamental abstraction to design pervasive systems its applicability for networks composed of up to hundreds of
[11], [2], [4]. A field is a function mapping each node of nodes, as it happens with pervasive computing domains [22].
a spatially distributed network of computing devices to a
(possibly structured) value, representing some aspect of the The remainder of the article is organized as follows. Section
local system state. It hence provides a viewpoint of distributed II details background on stochastic model checking; Section
computing algorithms as spatial computations, namely, as the III introduces the details of our modeling language and its
dynamic evolution of spatial data structures. As a reference translation into PRISM; Section IV discusses the application
example, a mobile agent can retrieve a device in a mobile and of our framework to some example algorithms; and finally
faulty network by “descending” the self-healing gradient (a Section V concludes providing final remarks.
II. A PPROXIMATE S TOCHASTIC M ODEL C HECKING “[label] guard -> r:(update)”, where guard is a
sequence of conditions that need to be satisfied to enable the
In recent years, there has been a growing interest on formal transition, r represents transition rate, and update is a list
models and verification of distributed, large-scale networks of operations to update (part of) the state of the system by
like those regarding pervasive computing. In this section, we modifying variables.
present approximate stochastic model-checking as a general Properties to verify are CSL formulas: for instance, prop-
tool to verify quantitative properties on distributed systems, erty “Which is the probability for variable state to
and in particular on computational field. reach value true within time T?” is expressed by formula
Stochastic Model Checking: Stochastic model checking “P=?[F<=T (state=true)]”, where F is the standard
[9] is basically the probabilistic extension of traditional future operator of temporal logic.
model checking [5]. It is based on probabilistic models Languages and Frameworks for Computational Fields:
such as DTMC (Discrete-Time Markov Chain) and CTMC Computational fields promote the viewpoint of conceiving
(Continuous-Time Markov Chain), which allow one to express algorithms for computer networks in terms of evolution of
the likelihood of the occurrence of certain transitions an distributed data structures.
algorithm (or system behavior) is composed of—in this article Proto [1] is a reference language for modeling and imple-
we deal with CTMC, for we shall consider (continuous) time menting spatial computing systems, featuring the notion of
an important aspect of system modeling. Verification over such computational field as a primary abstraction. Proto allows to
systems basically amounts to computing the overall probability define the behavior of single devices within a network, located
of the set of paths that satisfy the logic formula of interest, at specific points in a continuous space. For instance, the
expressed in a suitable probabilistic temporal logic, e.g. CSL specification:
(Continuous Stochastic Logic) [10]: for instance, we might ask
(rep d (inf) (mux (sense 1) 0
questions like “will the system eventually reach state S with a (min-hood (+ (nbr-range) (nbr d))))
probability greater than 80%?”, or “which is the probability )
for the system to stay in state S for at least 1 hour?”.
associates each node of the network with its overall distance
Approximate Verification: A major drawback of model from a source node where sense operator is activated.
checking is state-space explosion: as a system grows in size, Variable d is initialized to infinite, and updated to 0 where
the number of states quickly diverges, easily making model sense is activated (source node). In any other node n, the
checking unfeasible in practice. Given the size of systems variable is assigned with the minimum value of d (as computed
modeling large networks (as typical in pervasive computing), in any neighboring node n0 ), plus the distance between n and
exact model checking would be impractical: hence, it is n0 .
necessary to consider approximate techniques. The applicability of computational fields for pervasive com-
Approximate model checking is basically about running puting has already been studied and detailed in the series of
a large set N of simulations per test case, with specific works concerning the TOTA (Tuples On The Air) infrastruc-
techniques to obtain statistic information out of them that can ture [12], and recently in the context of chemical tuple spaces
be interpreted as a model-checking (search in the whole state [17], [18] and pervasive service ecosystems [19], [21].
space) done with a given approximation and confidence δ—
computed as N ≥ 4log( 2δ )/2 [7]. As a realistic example, III. F RAMEWORK
= 10−2 and δ = 10−3 require N ≈ 1300 000 number The framework presented here allows to model computa-
of independent simulations. By this technique one can in tional fields in pervasive and spatial systems via a specification
principle answer the same questions as in standard stochastic language based on the concept of transition. This is basically
model checking, yet trading-off simulation time with qual- a variant of the PRISM language, capturing the concept of
ity of the result (approximation/confidence),namely, obtaining “networked set of nodes”. A generation process translates the
results with high confidence and good approximation may model into a PRISM CTMC module, and then builds a com-
require time-consuming simulations performed by generating plete PRISM specification representing the whole network,
a large number N of simulation runs. On the other hand, the composed of as many PRISM modules as the number of nodes
problem is state-space explosion is avoided, and hence bigger (devices) in the network: to this end, module renaming – a
networks can typically be tackled. In the following we hence mechanism proper of PRISM – is exploited whenever possible
mostly deal with approximate stochastic model checking— to reduce code expansion. In other words, the framework
which is simply referred to as stochastic model checking. essentially provides the necessary support for modeling com-
PRISM: One of the most well-known probabilistic model putational field algorithms via a transition-based specification
checker – which we will rely upon in this article – is PRISM language, along with properties, rewards, and formulas. In
[8]. PRISM models are specified in terms of modules whose particular, the specification language allows one to model
behavior is expressed by transition rules and whose state is each device in a pervasive system as a set of transition rules
encoded in a set of discrete variables. In CTMC, transitions whereby the device – through observation of its neighbors –
are associated with a rate and can be labelled—transitions with can change its state and/or influence the state of the neigh-
same label are synchronized. A transition follows the syntax bors. This mechanism is key to both model self-adaptativity
S ::= D T
(changing system behavior only through local interactions) and D ::= X : [n_l..n_u];
context-awareness (system behavior intrinsically depends on T ::= [L] P --e--> A;
the local context) [20]. Finally, also properties, rewards and A ::= V’=e
P ::= b | N:=&f[e] | N:=&f[b]
CSL formulas are translated into the corresponding PRISM f ::= any | min | max
components, so as to obtain a comprehensive PRISM specifi- e ::= r | V | (e) | e+e | e-e | e*e | e-e | -e | f[e]
cation ready to be model checked. b ::= e<=e | e=e | e>e | e=e | e!=e
V ::= X | M.X | @.X
A. Architecture
Fig. 1. Syntax of the specification language for computational fields.
The components of the framework are essentially a language
translator and a PRISM generator. The language translator
takes a specification written in our language – defining the
behavior of a generic node in the pervasive network – and pro-
In our language, a model specification S is essentially a list
duces a corresponding PRISM template specification, which
of variable definitions D followed by behavior definition, i.e.
cannot yet be correctly parsed by PRISM, since some parts
a list of transitions T. New variables are introduced declaring
of the generated code are left unspecified: those are the parts
their name X, a lower bound n_l and an upper bound n_r.
involving actions related to neighbors. To this end, the PRISM
Transitions provide a list of preconditions P to be checked, a
generator takes a description of the network topology, along
numerical markovian rate specified via a numeric expression
with a file containing the properties, rewards, and formulas to
e, and a list of updates A, formed by assignments.
be verified, as input arguments . It then creates a complete
PRISM code to be verified, as shown in Section IV. An assignment V’=e is used to update the state of a variable
As regards network generation, two basic modalities are with an expression e—see below for the actual shape of
possible. On the one hand, a set of fixed topologies are variables and expressions. Notation V’ is retained as a PRISM
available: (i) square grid, (ii) square grid with diagonal links, legacy to mean the new value that V will take.
and (iii) hexagonal grid. Additional parameters to be set in this A precondition P is either a boolean expression b, or an
case include: number of nodes, torus structure (nodes at the assignment of kind N:=&f[e] or N:=&f[b]: this assigns N
boundary of the grid are connected to those on the opposite with the identifier of the node selected by function f based
side), and probability for each potential link to be actually on the result of expression evaluation. Cases currently sup-
present—the latter is especially useful when modeling real ported include: N:=&any[b], meaning that any node where
domains, as it allows to tackle the heterogeneity typical of real b is positively evaluated is non-deterministically selected;
environments. Though we found the above cases covering a N:=&max[e], meaning that the node having the greatest
wide set of scenarios for experiments, we also allow ad-hoc value resulting from evaluation of e is selected; and similarly
topologies: in this case, the user has to provide an external for N:=&min[e].
file indicating the actual network structure to adopt, which is
defined as the set of node pairs modeling links. Finally, it is Numerical expressions include real numbers, variables, ap-
possible to compactly define the initial states of nodes, i.e. of plication of function f as above (yielding any, maximum or
their variables as described below. minimum value of an expression in the neighborhood), and
any combination of them by standard mathematical operators
B. Language Syntax and parenthesis. Similarly, boolean expressions are obtained by
We now introduce our specification language for computa- combining numerical expressions with comparison operators.
tional fields. This language is state- and transition-based like Finally, and most importantly, variables can be qualified in
that adopted in PRISM: however, despite PRISM, there is no three ways: X refers to a local variable, M.X to variable
concept of module, as our language simply aims at abstractly X in node M, and finally @.X refers to variable X in the
describing the behavior of a generic node in a pervasive currently considered neighboring node. Informally, when used
network. Furthermore, in order to support computational field outside the scope of a function f, @.X basically spawns
modeling, the language is provided with constructs that make one copy of the transition per neighboring node, otherwise it
it possible to describe the behavior of a node by referring to denotes the neighbor considered by function f. For instance,
nodes in its neighborhood. N:=&any[X>@.X] selects one neighboring node in which
The syntax of the language is reported in Figure 1, where variable X is smaller than the local one, assigning its identifier
r is a meta-variable over real numbers, L over label names, to N for future use. Finally, as additional details not explicitly
X over variable names and M over node names (conceived reported in the syntax, it is worth remarking that N:=&f[e]
as alphanumeric sequences). Notation x is generally used to can appear just once in list P, and function f[e] cannot
denote a possibly empty list of elements of type x: in partic- contain another nested f[e].
ular, D stands for D1 . . . Dn , T stands for T1 . . . Tn , P stands For the sake of space, the details related to translating our
for P1 & . . . & Pn , and A for A1 & . . . & An . Additionally, as specification language into PRISM are introduced via simple
concerns the latter two cases, the empty list is represented by examples, which are sufficient enough to grasp the necessary
term true. details.
C. Example translations that represents the specification for a node of the network
Diffusion: As a first paradigmatic example to show the identified as node_1, which is the source of the random walk
details of translation into PRISM code, we adopt the case of (value_1 set to 1). The neighbors of this node are node_2
a computational field defining the diffusion of a sample value and node_3. In particular, rules move_1_2 and move_1_3
(1) so as to cover the whole network: initially, such a value is model the nondeterministic choice of one of the neighbors of
present only in one node, referred to as source. The complete node_1 satisfying condition @.value=0: this condition is
specification modeling diffusion is simply: translated into guards value_2 = 0 and value_3 = 0
appearing in rules move_1_2 and move_1_3, respectively.
value : [0..1]; Put simply, the nondeterministic choice specified in our lan-
[diff] value=0 -- 1.0 --> value’= max[@.value];
guage via any[@.value=0] is modeled in PRISM as a
where value represents the value to be spread across the race between the move_i_j transitions satisfying condition
network: it is set to 1 in the source and 0 elsewhere. Diffusion value_j= 0, where i denotes current node and j ranges
occurs via rule diff: each node with value = 0 keeps among neighbors of i.
updating value at rate 1.0 by choosing the greatest value Once a transition is chosen, the corresponding update is exe-
among its neighbors. As a result, value 1 spreads across the cuted, so as to set value_1 to 0. The value in the chosen node
whole network, until completely covering it. The correspond- has still to be set to 1: this cannot be done directly in the mod-
ing PRISM code for one node of the network, produced by ule of node_1, as PRISM does not allow to change the value
the generator, is of variables defined in modules external to the current one.
module node_1 It is then necessary to exploit PRISM synchronization, that
value_1 : [0..1] init 1; makes it is possible to update variables in external modules
[diff_1] value_1=0 -> 1.0 : by synchronizing transitions with the same name in different
value_1 = max(value_3,value_2,value_4);
endmodule modules, that are then executed simultaneously. Accordingly,
each neighbor j of node i is as well provided with a transi-
where value_1 represents the value to be spread on the tion “[move_i_j] true -> 1.0 : (value_j’=0)”,
network in node_1: it is worth noting that this node is the which is always enabled and executed together with the corre-
source since value_1 is initialized to 1. The neighborhood sponding move_i_j rule defined in the module of node_i.
of each node is entirely created by the generator in an
automatic fashion, in accordance with the chosen topology. D. Property Specification and Rewards
In rule diff_1, value’=max[@.value] is translated
into value_1’=max(value_3,value_2,value_4): Our specification language allows to specify properties
value_2, value_3, and value_4 are the values in the and rewards. On the one hand, properties are a necessary
neighbors of node_1. Function max is a built-in PRISM component to perform verification, as they identify states
function returning the greatest of its arguments: the returned of interest whose probability to occur can be analyzed via
value is then assigned to value_1. stochastic model checking. On the other hand, rewards make
Random Walk: This example models the random movement it possible to further extend computational field analysis,
of a reference value (again, 1) across the network, starting from making it possible to not only reason about probabilities for
a source node toward a node designated as the target of the a model to behave in a certain fashion, but also quantitatively
“walk”. The corresponding specification is: measure cumulative performance parameters regarding system
behavior—e.g., how many times a transition fired.
value : [0..1]; target : [0..1];
[move] value=1 & N:=&any[@.value=0] A property is expressed as
-- 1.0 --> “property "name" = Q [ Bexp ];”, defining a
value’=0 & N.value’=1; new property name, where Q represents a quantifier on
where value represents the value to be moved across the Bexp, which is a PRISM boolean expression over model
network, and target = 1 is adopted to denote the target node variables. The quantifiers that can be adopted are forall
of the walk. After choosing non-deterministically a neighbor and exist, meaning that Bexp must be satisfied for every
where value = 0, rule move updates its local state by setting node of the network and for at least one node of the network,
local value to 0, and value on the neighbor to 1. The respectively. Typical logical connectives among variables
translation into PRISM results in this code: adopted in boolean expressions are: and (represented by
symbol &), or (symbol |), and not (symbol !). An example
module node_1
value_1 : [0..1] init 1; of property specified on diffusion is:
target_1 : [0..1] init 0; property "diffusion_complete" = forall[value=1];
[move_1_2] value_2 = 0 -> 1.0 : (value_1’=0);
[move_1_3] value_3 = 0 -> 1.0 : (value_1’=0);
stating that diffusion is complete in every node of the network.
In the random walk example the following property can be of
[move_2_1] true -> 1.0 : (value_1’=0); interest:
[move_3_1] true -> 1.0 : (value_1’=0);
endmodule property "target_reached" = exist[target=1 & value=1];
It states that the target of the random walk has been reached
if there exists a node where target = 1 (denoting the target
node) and value = 1. A property is then simply translated
into a PRISM label, a construct denoting specific system states.
For instance, diffusion_complete is translated into this
PRISM label:
label "diffusion_complete" =
(value_1=1) & (value_2=1) & ... & (value_n=1);
(a) (b)
which is a simple expansion of the property specified in our
specification language.
Rewards adopt a syntax similar to that used in PRISM re-
wards: from a practical viewpoint, a reward in our specification
language is a compact form of a PRISM reward. As a reference
example, consider the following reward, called hops, defined
on diffusion:
rewards "hops" = [diff] true : 1;
which increments hops by 1 at each execution of diff in (c) (d)
any node of the network. This is translated into the PRISM
reward: Fig. 2. Example of gradient diffusion on a 4x4 random torus topology.
rewards "hops"
[diff_1] true : 1; ... [diff_n] true : 1; pump : [0..1]; field : [0..MAX];
endrewards
[] pump=1 & field>0 -- 1.0 --> field’= 0;
[diff] pump=0 -- 1.0 --> field’= min[@.field]+1;
IV. M ODEL C HECKING C OMPUTATIONAL F IELDS
Fig. 3. Specification of the gradient algorithm.
Based on the above discussed specification language and the
associated properties/rewards, we here present some paradig-
matic examples of computational fields, and accordingly show number of connections in the neighborhood of a node is 4. This
the resulting analysis performed via stochastic model check- topology is hereafter referred to as random torus.
ing. For each example, we show the corresponding model
specified in our language, a description of the important
A. Gradient Diffusion
properties to be analyzed and verified, and finally the results
obtained via model checking of those properties in PRISM. Gradients are a particular kind of computational field where
Reference Topology: For the sake of uniformity and sim- the value of the field in a given node depends solely on a notion
plicity in presenting the experiments, we find it useful to of “distance” from the so-called gradient source node. Here,
consider one reference network topology to use. Although the we consider a gradient where field is represented by an integer
choice may evidently affect the results of model checking, value, denoting the distance in terms of minimum number of
and many topologies could be considered and compared, we hops from the source. The gradient is completely established
here stick to a single case, which we consider to be of a when all nodes are “covered” with a proper field value. Figure
general validity for the context of pervasive systems. On the 2 shows an example of gradient diffusion on a 4x4 random
one hand, locations are placed as nodes in a grid network, torus topology.
such that each location has in its proximity 8 nodes, 4 in the Gradients are actually useful in pervasive domains, in sit-
horizontal/vertical direction, and 4 in the diagonal direction— uations where it is necessary to find a (minimum) route to a
nodes at the boundary of the grid are connected to the nodes on specific device in the network, as well as a basic pattern to
the opposite side (both in the horizontal/vertical and diagonal form virtual communication channels between nodes that need
directions) so as to form a torus. This choice is motivated to interact with one another. In general, gradient is the basic
by the fact that very often computing devices are placed brick to inject self-organization in a network, making a local
more or less uniformly over the space formed by buildings, situation affect a system in a more global way through (pos-
corridors, or rooms of the pervasive computing systems of sibly selective) propagation [3]. Furthermore, gradient-based
interest. On the other hand, exceptions to this case are the algorithms can be implemented in order to be flexible, i.e.
norm, hence we introduce some randomness in the topology able to adapt to changes in the network, such as node failures,
to tackle heterogeneity of the environment, as well as failures connection changes (reflecting node mobility), and new nodes
and so on. Accordingly, links between nodes are chosen in a entering the network: the gradient algorithm modeled in the
random way: namely, the probability that a node is connected next is shown to be able to reconfigure in response to changes
to one of the 8 in its proximity is 50%: in this way, the average in the network.
Gradient Model: Figure 3 shows a simple model of gradient of number of hops. In order to measure the number of
diffusion specified through our formal language: the model hops needed to establish the gradient, it is possible to define
simply defines the behavior enforced in each node of the a reward, which allows to reason on quantitative measures
network—it is similar to the Proto example shown in Section regarding model behavior. Expected number of hops can be
II. Variable pump is an integer value used to denote the considered by introducing the following reward:
source of the gradient: it is initialized to 1 in the source rewards "hops" = [diff] true : 1;
node and set to 0 in every other node. The field variable
represents the actual value of the gradient in a node: it is that assigns a reward of 1 to every execution of transition
initially set to MAX in every node, where MAX is a value diff in any of the nodes composing the network.
higher than the maximum value the gradient can reach once Experimental Results: Based on the properties identified
completely diffused in network—the so-called diameter of above, here we show some of the results obtained by applying
the network. Put simply, nodes not yet reached by gradient approximate stochastic model checking on the gradient algo-
diffusion will have field = MAX. The behavior of each node rithm, for different network instances. Given the large size of
is essentially specified by two rules: the first applies only on the model instances verified, approximate model checking was
the source node, resulting in setting the value of the gradient adopted. To this end, we chose an approximation = 10−2
to 0. The second rule (diff) is applied on other nodes of and a confidence δ = 10−3 : this means that the probability
the network, and set field to 1 plus the minimum value of for the obtained results to be affected by an error less than
the gradient among the neighboring nodes. It is worth noting (or equal to) 10−2 is greater than 99.9%. According to the
that these rules are continuosly executed at markovian rate formula described in Section II, the corresponding number
1.0 in each node—namely, the time between two executions of runs required to meet these approximation and confidence
is drawn by a negative exponential distribution of probability, values is about 1300 000.
following the well-known memoryless property. This means The first property verified on the gradient algorithm con-
that each node updates in an independent and asynchronous cerns the time necessary for the gradient to be completely
way with respect to others, so that gradient diffusion and established in the network. This is specified by the following
its consequent stabilization are achieved by emergence: this CSL-like property expressed by the PRISM syntax:
also allows gradient to self-adapt to changes occurring in P=? [true U<=k "established_gradient"]
the network. Indeed, if e.g. a node disconnects from the which is a bounded-until path property, simply returning the
network, its neighboring nodes are able to automatically and probability to achieve the established_gradient state
independently update their gradient value. within k time units. This property was verified against different
Properties to Verify: Among the different properties we 5xN random torus instances, with N ∈ {5, 10, 15, 20, 25} and
may be interested to analyze on a gradient, one of the most k ranging from 0 to 30 time units: the corresponding results
important is undoubtably how long it takes for a gradient are shown in Figure 4 (a). For each instance, the probability of
to completely spread over all the network and get stable. achieving the established_gradient state gets 1 after a
For instance, if you think of a gradient exploited to diffuse certain time—still considering the approximation due to and
information about a specific device or to establish a connection δ. Before that stabilisation time, probability of convergence is
between two devices, it is important to know how long it of course smaller than 1. Figure 4 (b) shows the trend of the
is needed for the gradient to cover the network. A gradient minimum time necessary to achieve an established gradient
is completely established and stabilized when for each non- with probability 1 over the different investigated instances: it
source node i of the network (i.e. where pump = 0), variable is easy to see that minimum time increases in a (quasi) linear
field is precisely 1 plus the minimum value of field in way as the size of the network grows.
the neighborhood. Accordingly, in our language we can define As regards verifying the expected number of hops needed to
the following property: establish the gradient, the following reachability reward-based
quantitative property was exploited:
property "established_gradient" =
forall[ (pump=0 & field=min(@.field)+1) | R{"hops"}=? [ F "established_gradient" ]
(pump=1 & field=0) ];
that – according to the "hops" reward structure –
A further property that would be interesting to analyze returns the expected number of hops to achieve the
on the network concerns the cost for the gradient to get established_gradient state. Figure 5 (up) reports the
established, expressed in terms of network hops necessary expected number of hops to establish the gradient, obtained
for the gradient to spread across the whole network. Often, from verifying the property on the same 5xN random torus
in pervasive scenarios, communication among devices can instances adopted in previous experiments: it is easy to rec-
be really expensive due to power/battery constraints, so that ognize a linear increase.
being aware of the number of hops necessary for completely We now describe an important issue concerning the com-
establishing a gradient becomes important. This is perhaps plexity of model checking from the standpoint of time: un-
crucial also in order to trade off performance (time necessary derstanding how much time it takes to verify properties is
to establish the gradient) and cost—expressed here in terms fundamental to assess feasibility of model checking. Figure
B. Gradient Descent
We here consider another key algorithm for computational
fields (see e.g. [12]) aimed at supporting data retrieval in per-
vasive computing scenarios, allowing data to follow downhill
a gradient until reaching its source. This can be useful for
retrieving specific information/services in spatially distributed
networks of devices: e.g. a user starts diffusing a gradient con-
taining a query for the specific information/service she/he is
interested in: once the gradient reaches the location containing
the sought information, such information follows downhill the
gradient until coming to its source, i.e. the location of the user
requiring the information/service.
In the example reported below, gradient descent occurs in a
probabilistic way: the sought information follows the gradient
by choosing probabilistically a direction where the gradient
value is low. In other words, the lower the gradient value of
a node in the neighborhood of the current one, the higher the
probability for the sought information to move to that node.
Gradient Descent Model: The behavior to be enforced
in each node of the network, modeling gradient descent, is
defined according to the specification reported in Figure 7. The
Fig. 4. Probability of achieving an established gradient over time on different
5xN random torus instances (up), and minimum time necessary to achieve the information descending the gradient is represented through
established gradient with probability 1 over the different instances (down). variable desc set to 1: initially, desc is 1 in the target node,
and 0 elsewhere. As soon as the gradient reaches the target
node, information starts descending the gradient by rule move:
this is modeled by making value 1 of desc move across the
network, following downhill the gradient. This rule applies
to nodes where desc = 1. It states that any neighbor with
a lower gradient value (&any[@.field0 -- 1.0 --> field’= 0;
[diff] pump=0 -- 1.0 --> field’= min[@.field]+1;
[move] desc=1 & N:=&any[@.field
desc’=0 & N.desc’=1;
Fig. 7. Specification defining gradient descent.
Fig. 9. Segregation: sample runs on a 15x15 random torus showing two
possible spatial distributions of regions, starting from data sources placed at
the corners of the network (left) and as an “inverted T” (right). Numbers
represent the position of the sources of the different data kinds.
simply returning the probability of achieving the
descent_complete state within k time units. This
property was verified on different 5xN random torus
instances, with N ∈ {5, 10, 15, 20} and k ranging from 0 to
80 time units: in each instance, gradient source and target
(represented by desc= 1) were placed at the maximum
practicable distance, which is dN/2e on the adopted topology.
The corresponding results are shown in Figure 8 (up). There,
it can be seen that, for each instance, the probability of
getting the descent_complete state becomes 1 after
a given time, representing the minimum time needed for
completing the descent. The corresponding trend is reported
in Figure 8 (down): time increase is polynomial with instance
size.
As in the case of gradient diffusion, we can also verify
Fig. 8. Probability of descending a gradient and coming to its source over the expected number of network hops necessary to complete
time on different 5xN random torus instances (up), and corresponding trend gradient descent, by using the descending_hops reward.
of the minimum time necessary to come to gradient source with probability
1 over the same instances (down). The corresponding results on the 5xN random torus instances
are: 3.021 hops necessary on the 5x5 instance, 5.025 on the
5x10, 7.119 on the 5x15, and 10.016 on the 5x20. As in the
some kind of information (represented by desc) starts with case of gradient diffusion, these results correspond to a quasi
gradient diffusion and gets completed when the information linear increase with instance size.
arrives to gradient source (the requesting node). We can state
that gradient descent is finished if the desc = 1 condition C. Segregation
applies in the source node, namely: Segregation is a further computational field algorithm based
property "descent_complete" = exist[pump=1 & desc=1]; on gradients, conceived to diffuse data across pervasive net-
works: here, the objective is to keep data of a certain kind
Again, as a further property, it is also interesting to analyze segregated from data of different kinds so as to form spatial
the number of network hops needed for desc to reach the regions characterized by data organized per kind. In other
source. This is simply obtained by assigning a reward of 1 words, it is possible to conceive a network where several gra-
to transition move as in previous subsection—this reward is dient sources are placed in different nodes, one per data kind.
hereafter referred to as descending_hops. Such different kinds of data are then diffused on the network,
Experimental Results: Approximate model checking on stopping where another region is found so as to ultimately
gradient descent was executed with the same confidence and partition the whole network without overlaps. Examples of
approximation values chosen for gradient diffusion. The first segregation on a 15x15 random torus are reported in Figures
verified property was the time needed for desc to completely 9 (left) and (right), showing the final data organization starting
descent the gradient, which can be expressed according to the from gradient sources placed at the corners of the network and
CSL formula: as an “inverted T”, respectively. This is for instance useful
P=? [true U<=k "descent_complete"] in pervasive service scenarios, to support spatial competition
among services providing the same functionality: in fact,
segregation can support competition, allowing services to
organize and satisfy user requests by adaptively organizing
their distribution on the network.
Segregation Model: A model for segregation is shown in
Figure 10. The only additional variable with respect to gradient
model is segr, whose value represents the data kind stored
in a given node. In this model, segr ranges from 0 to 4,
meaning that we are considering four different kinds of data
(from 1 to 4) to be diffused in the network—0 denotes a node
containing no data, i.e. a node not yet reached by diffusion
of any kind of data. Segregation is actually modeled via rule
spread, simply stating that the data kind hosted by current
node will be that of any of its neighbors with a smaller gradient
value: as usual, this neighbor is designated as N, and its value
set to &any[@.field 0 ]; configurations can anyway be exploited. The corresponding
results are reported in Figure 11 (up): it is easy to recognize
which states that all the nodes of the network need to have a
that, after a certain time, probability of completing segregation
value of segr > 0, meaning they all host a certain kind of
becomes 1 for all the instances. Complementarily, Figure
data.
Additionally, it would be worth also to analyze the expected 11 (down) shows the trend of the minimum time needed to
size achieved by the various regions formed as a result of data complete segregation with probability 1 over the analyzed
diffusion: the size of each region depends on the location of instances: the corresponding time increase is quasi linear.
the corresponding data source. To measure this property for As regards the expected size of each formed region i (where
the region formed by diffusion of data kind i, we need to i denotes data kind), we relied on the following cumulative
define a reward such as: reward-based property:
R{"region_i_size"}=? [ I = k ]
reward "region_i_size" = (segr = i) : 1;
where i represents the data kind to analyze. This reward that returns the sum of rewards cumulated concerning region
assigns a reward of 1 to each node where segr = i, i.e. i at time k. Constant k has to be chosen carefully: it has to
hosting data kind i. be at least equal to the minimum time at which the probability
Experimental Results: Approximate model checking on of achieving complete segregation becomes 1. This value can
segregation was again performed with the usual confidence and be inferred by looking at the results shown in Figure 11. The
approximation values. We initially verified total time necessary results obtained by verifying this property on a 10x10 random
for completing segregation, as previously described. To this torus (with data sources placed to form an “inverted T” like in
end, the following CSL property was adopted: Figure 9 (b)) are: 25.61 nodes for data kind 1, 15.63 for kind
2, 30.86 for kind 3, and 29.87 for kind 4. The expected region
P=? [true U<=k "segregation_complete"]
size varies a lot among the different regions: in particular, the
simply returning the probability of achieving the region formed by data kind 2 has a noticeable lower expected
segregation_complete state within k time units. number of nodes as the corresponding source position limits
This property was verified against different NxN random the space available for diffusion, which is constrained by the
torus instances, with N ∈ {5, 10, 15} and k ∈ [0, 40], starting close proximity of data sources 1 and 3.
pump : [0..1]; field : [0..MAX]; segr : [0..4];
[] pump=1 & field>0 -- 1.0 --> field’= 0 ;
[diff] pump=0 -- 1.0 --> field’= min[@.field]+1;
[spread] N:=&any[@.field
segr’=N.segr;
Fig. 10. Specification of the segregation algorithm.
V. C ONCLUSION AND F UTURE W ORK [6] J. L. Fernandez-Marquez, G. Di Marzo Serugendo, S. Montagna, M. Vi-
roli, and J. L. Arcos. Description and composition of bio-inspired design
To the best of our knowledge, this article represents the patterns: a complete overview. Natural Computing, May 2012. Online
first explicit attempt to deal with modeling and verification First.
[7] T. Hérault, R. Lassaigne, F. Magniette, and S. Peyronnet. Approximate
of computational field algorithms, which are basic buildling probabilistic model checking. In Proc. 5th International Conference on
blocks for pervasive computing domains as studied in [11], Verification, Model Checking and Abstract Interpretation (VMCAI’04),
[2]. To this end, a specification language and a framework volume 2937 of LNCS. Springer, 2004.
[8] A. Hinton, M. Z. Kwiatkowska, G. Norman, and D. Parker. Prism:
for stochastic model checking were provided, that are targeted A tool for automatic verification of probabilistic systems. In TACAS,
at quantitative analysis of computational fields. As concerns volume 3920 of Lecture Notes in Computer Science, pages 441–444.
stochastic model checking, we relied on the PRISM proba- Springer, 2006.
[9] M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic
bilistic model checker (which was also an obvious inspiration model checking with prism: a hybrid approach. International Journal
to our syntactic and semantic approach), showing how the on Software Tools for Technology Transfer (STTT), 6(2):128–142, 2004.
proposed specification language can be translated into PRISM [10] M. Kwiatkowska, G. Norman, and D. Parker. Stochastic model checking.
In M. Bernardo and J. Hillston, editors, Formal Methods for the De-
code, so as to provide an easy way to perform quantitative sign of Computer, Communication and Software Systems: Performance
analysis. Evaluation (SFM’07), volume 4486 of LNCS (Tutorial Volume), pages
Our verification framework can be upgraded with new 220–270. Springer, 2007.
[11] M. Mamei and F. Zambonelli. Field-based Coordination for Pervasive
ingredients. A notable example would be the introduction of Multiagent Systems. Springer Verlag, 2006.
mechanisms to model node failures and mobility, so as to [12] M. Mamei and F. Zambonelli. Programming pervasive and mobile
verify aspects concerning with self-adaptation to probabilistic computing applications: The tota approach. ACM Trans. Softw. Eng.
Methodol., 18(4), 2009.
events. Then, the flexibility and expressiveness of our language [13] A. Omicini, A. Ricci, and M. Viroli. An algebraic approach for
should be extended to deal with a wider set of algorithms: modelling organisation, roles and contexts in MAS. Applicable Algebra
as such, it would be interesting to evaluate the possibility in Engineering, Communication and Computing, 16(2-3):151–178, Aug.
2005.
of translating Proto [1] and the eco-law lanaguage of the [14] A. Omicini, A. Ricci, and M. Viroli. Coordination artifacts as first-class
SAPERE appraoch [19] into PRISM using our language as abstractions for MAS engineering: State of the research. In Software
an intermediate step. Alternatively, it would be interesting Engineering for Multi-Agent Systems IV: Research Issues and Practical
Applications, volume 3914 of LNAI, pages 71–90. Springer, Apr. 2006.
to turn existing simulators like e.g. A LCHEMIST [16] into [15] A. Omicini, A. Ricci, and M. Viroli. Artifacts in the A&A meta-model
approximate stochastic model-checkers. Finally, it would be for multi-agent systems. Autonomous Agents and Multi-Agent Systems,
of general interest to devise a methodology for applying 17(3), June 2008.
[16] D. Pianini, S. Montagna, and M. Viroli. A chemical inspired simulation
stochastic model checking to multiagent systems, which we framework for pervasive services ecosystems. In Proceedings of the
believe would enjoy the use of meta-models based on the Federated Conference on Computer Science and Information Systems,
notion of artifact [14], [15], [13]. pages 675–682, Szczecin, Poland, 18-21 September 2011. IEEE Com-
puter Society Press.
[17] M. Viroli and M. Casadei. Biochemical tuple spaces for self-organising
ACKNOWLEDGMENTS coordination. In Coordination Languages and Models, volume 5521 of
LNCS, pages 143–162. Springer-Verlag, June 2009.
This work has been supported by the EU-FP7-FET Proactive [18] M. Viroli, M. Casadei, S. Montagna, and F. Zambonelli. Spatial coor-
project SAPERE Self-aware Pervasive Service Ecosystems, dination of pervasive services through chemical-inspired tuple spaces.
under contract no.256873. ACM Transactions on Autonomous and Adaptive Systems, 6(2):14:1 –
14:24, June 2011.
[19] M. Viroli, D. Pianini, S. Montagna, and G. Stevenson. Pervasive
R EFERENCES ecosystems: a coordination model based on semantic chemistry. In 27th
Annual ACM Symposium on Applied Computing (SAC 2012), Riva del
[1] J. Beal. The MIT proto language. http://groups.csail.mit.edu/stpg/proto. Garda, TN, Italy, 26-30 March 2012. ACM.
html, 2008. [20] M. Viroli and F. Zambonelli. A biochemical approach to adaptive service
[2] J. Beal and J. Bachrach. Infrastructure for engineered emergence on ecosystems. Information Sciences, 180(10):1876–1892, May 2010.
sensor/actuator networks. IEEE Intelligent Systems, 21(2):10–19, 2006. [21] F. Zambonelli, G. Castelli, L. Ferrari, M. Mamei, A. Rosi, G. D. M.
[3] J. Beal, J. Bachrach, D. Vickery, and M. Tobenkin. Fast self-healing Serugendo, M. Risoldi, A.-E. Tchao, S. Dobson, G. Stevenson, J. Ye,
gradients. In R. L. Wainwright and H. Haddad, editors, SAC, pages E. Nardini, A. Omicini, S. Montagna, M. Viroli, A. Ferscha, S. Maschek,
1969–1975. ACM, 2008. and B. Wally. Self-aware pervasive service ecosystems. Procedia CS,
[4] J. Beal, S. Dulman, K. Usbeck, M. Viroli, and N. Correll. Organizing 7:197–199, 2011.
the aggregate: Languages for spatial computing. CoRR, abs/1202.5509, [22] F. Zambonelli and M. Viroli. A survey on nature-inspired metaphors
2012. for pervasive service ecosystems. International Journal of Pervasive
[5] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The Computing and Communications, 7(3):186–204, 2011.
MIT Press, January 2000.