A Fo mal P og amming F amewo k o Digi al
A a a s?
Alejand o P´e ez-Ve eda, Ca los Canal, and E nes o Pimen el
Uni e si y o Malaga, Spain
[email p o ec ed],[email p o ec ed],[email p o ec ed]
Abs ac .
In he cu en IoT e a, he numbe o sma hings o in e ac
wi h is aising e e yday. Howe e , each one o hem p ecises a manual and
speci ic con igu a ion. In a mo e people- iendly scena io, sma hings
should adap au oma ically o he p e e ences o hei use s. In his
ield, we ha e pa icipa ed in he design o People as a Se ice, a mobile
compu ing e e ence a chi ec u e which endows he sma phone wi h he
capabili y o in e ing and sha ing a i ual p o ile o i s owne . Cu en ly,
we a e de eloping Digi al A a a s, a amewo k o p og amming in e ac-
ions be ween sma phones and o he de ices. This way, he sma phone
becomes a pe sonalized and seamless in e ace be ween people and hei
IoT en i onmen , con igu ing he sma hings wi h in o ma ion om he
i ual p o ile. In his wo k, we p esen a o maliza ion o Digi al A a a s
by means o a Linda-based sys em wi h mul iple sha ed uple spaces.
Keywo ds:
Digi al A a a s, People as a Se ice, PeaaS, Linda, Sha ed
Tuple Spaces.
1 In oduc ion
The In e ne o Things (IoT) is buil o e a laye o connec ed de ices and senso s
ha o e speci ic in e aces o access he in o ma ion hey collec and also o
con igu e how hey wo k, e.g. he equency o pick up he da a o how o o ma
hem [
9
]. Recen esea ch in he IoT ield has p omo ed he de elopmen o
de ices and senso s which a e mo e con igu able and p o ide easie in e aces.
They a e known as sma hings [
11
]. Howe e , sma hings s ill equi e a lo o
manual con igu a ion, and his p oblem becomes mo e challenging he bigge he
numbe o de ices we daily in e ac wi h. In a desi able scena io, he echnology
should wo k o he people and no he o he way a ound. E e y sma hing
should adap o he needs o he people seamlessly and in an au oma ic way,
educing he need o in e ac ion wi h he use s o he minimum.
Conside ing he pe asi e p esence o sma phones, he au ho s o his pape
ha e pa icipa ed in he design o a mobile compu ing e e ence a chi ec u e
?
This wo k has been unded by he Spanish Go e nmen unde g an s PGC2018-
094905-B-I00 and TIN2015-67083-R (MINECO/FEDER).
called People as a Se ice (PeaaS) [
10
]. This a chi ec u e p omo es he use o
sma phones o lea n abou hei use s, c ea ing and s o ing i ual p o iles wi h
hei p e e ences and con ex in o ma ion. These p o iles a e hen o e ed as a
se ice o hi d pa ies in a secu e manne . This way, sma phones become seam-
less and au oma ic in e aces ha nego ia e hei owne ’s p e e ences, adap ing
and con igu ing he sma hings in hei su oundings.
Fo ha pu pose, he equi ed in e ac ions a e no jus simple da a ans e s,
bu we need mechanisms ha allow o con igu e sma hings, and also o
comple e i ual p o iles wi h con ex knowledge ob ained om hese in e ac ions.
The mo e comple e i ual p o iles a e, he be e may he echnology adap
o he people. Wi h his goal in mind, we a e de eloping Digi al A a a s, a
dynamic p og amming amewo k which allows de ining he in e ac ions be ween
sma phones and sma hings by means o on- he- ly sc ip s [
13
]. The sc ip s a e
execu ed in he sma phone, and hey make use o he i ual p o ile s o ed in i
o econ igu ing he beha io o he sma hing wi h he in o ma ion a ailable.
Ou p og amming amewo k is inspi ed by he ision o a P og ammable
Wo ld [
17
], which o esees he e olu ion om oday’s IoT based on da a ecollec-
ion o uly p og ammable de ices. This way, bo h sma hings and sma phones
a e able o lea n om each o he , and o e ol e h ough each in e ac ion in a
anspa en and dynamic way.
In his pape , we p esen a o mal amewo k o Digi al A a a s. The ame-
wo k p o ides a o mal desc ip ion o i ual p o iles and he sc ip s o execu e on
hem, and i es ablishes he basis o issues like p i acy o secu i y, wi h secu e
connec ions con olling he access o i ual p o iles. The o maliza ion is based
on a mul iple sha ed uple spaces model inspi ed by Linda, which makes possible
o ensu e he soundness o he amewo k, and makes easible he analysis o
some in e es ing p ope ies.
The es o his pape is s uc u ed as ollows. In Sec ion 2 we p esen he
mo i a ions o his pape and discuss some ela ed wo ks. Nex , Sec ion 3 de ines
he concep s necessa y o eason on Digi al A a a s. In Sec ion 4, we o malize
he in e ac ions ha ake place in he amewo k and demons a e in e es ing
o mal p ope ies o he sys em. Then, Sec ion 5 p esen s a p oo o concep and
analyze i s implemen a ion using he amewo k. Finally, Sec ion 6 d aws he
conclusions o he pape and b ie ly discusses u u e wo k.
2 Backg ound
The de elopmen o sma hings is ans o ming people’s li es, as we inc easingly
in e ac wi h hem e e yday. Social Compu ing (SC) [
18
] is he a ea o compu e
science ha deals wi h he in e ac ion be ween social beha io and compu e
sys ems. SC encompasses all hose sys ems ha collec , p ocess and dissemina e
in o ma ion ela ed o indi iduals and g oups o people. The goal is lea ning
abou people and hei p e e ences and p o iding an easy adap a ion o hei IoT
en i onmen , educing manual con igu a ion o de ices o a minimum. Indeed, a
numbe o ecen esea ch wo ks ag ee on gi ing suppo o he IoT by means o
a pa adigm ocused on people [16].
Cu en ly, e y ew companies a e able o access and p ocess his eno mous
quan i y o social in o ma ion, and o exploi and make a p o i om i . In
p ac ice, his educes he SC ma ke place o a small numbe o big s akeholde s.
As Tim Be ne s-Lee decla ed ecen ly [
1
], SC sys ems should empowe people,
making hem he ai owne s o hei in o ma ion, and deciding who has access
o i . Mo eo e , his in o ma ion mus be s o ed in a unique and accessible place
which le s hi d pa ies use i in a con olled way, ollowing he p i acy p e e ences
o he use s.
In his same sense, we ad oca e o de eloping collabo a i e a chi ec u es
based on sma phones. Thei pe asi e p esence in people’s e e yday li es and
hei inc easing senso ing and compu ing capabili ies, oge he wi h hei com-
munica ion skills, make hem key elemen s o ob aining, p ocessing, and sha ing
in o ma ion abou hei use s [
15
]. Sma phones a e also he mos app op ia e
de ices o be in cha ge o nego ia ing he in e ac ions o hei use s wi h sma
hings in hei en i onmen .
A chi ec u es based on P2P models a e g adually acqui ing a g ea e p esence
in ields such as social ne wo ks [
19
] o ecommenda ion sys ems [
20
]. The basis
o hese a chi ec u es a e he i ual p o iles o he use s, plen y o con ex ual
da a (e.g. ac i i ies, ela ions wi h o he use s, e c.) [
8
]. Ou goal is sha ing
hese i ual p o iles wi h hi d pa ies and o adap he IoT en i onmen o he
p e e ences and needs o each use .
Wi h ha pu pose in mind, ou app oach is based on a Linda-like model.
Linda [
7
] is a coo dina ion language whe e synch oniza ion is achie ed by means
o a sha ed uple space, and h ough a se o simple bu enough exp essi e
p imi i es [
2
]. Howe e , a single sha ed uple space would iola e he p inciples
o he PeaaS model. Some o he Linda-like p oposals ha e been made by di e en
au ho s, in oducing some kind o mobili y, mainly based on adding capabili ies
o emo ely modi ying a gi en uple space. Thus, Lime [
14
] was p oposed as a
Linda ex ension o suppo mobile compu ing, by he de ini ion o ansien ly
sha ed dis ibu ed uple spaces o es ablish P2P communica ions. Some o i s
goals a e common wi h ou s, bu ou amewo k also akes in o accoun p i acy
issues, which a e c ucial o i ual p o iles. Ano he well-known p oposal is
KLAIM [
5
], which ex ends Linda by conside ing he possibili y o emo e adding
uples o an accessible uple space. Wi h a simila philosophy, SCEL [
6
] was
designed o p o ide a pa ame ic language o cap u e a ious p og amming
abs ac ions o au onomic componen s and hei in e ac ion. In bo h cases,
Linda-like p imi i es we e added o allow he emo e in e ac ion wi h sha ed
uple spaces. Al hough he PeaaS pa adigm could be (a i icially) coded by hese
languages, a numbe o assump ions and cons ain s should be made o ensu e
he main PeaaS ea u es. In ac , we conside ha accessing o a i ual p o ile
has o be made only by i s owne , and emo e accessing o ansien uple spaces
o sha ed eposi o ies do no model hese scena ios p ope ly.
3 Modeling Digi al A a a s
In o de o de ine a o mal amewo k o easoning on Digi al A a a s, we
in oduce he no ion o i ual p o ile oge he wi h a numbe o ela ed concep s,
and we desc ibe how i ual p o iles can be o e ed as se ices unde he PeaaS
pa adigm.
3.1 De ini ions
The key issue o aking in o accoun he use in an IoT en i onmen is he
i ual p o ile. I con ains in o ma ion abou use p e e ences, habi s, mo emen s,
o ela ions. All his in o ma ion is only s o ed in he use ’s de ice (e.g. a
sma phone), and i is o e ed as a se ice o hi d pa ies. The de ini ion below
o malizes his no ion.
De ini ion 1.
A i ual p o ile
P
is a mul ise o en i ies, whe e each en i y
is a 5- uple
= (
n, s, p, , s
)composed o (i)
n∈Name
ep esen ing he name
o he en i y, (ii)
s∈Type
de ines he en i y’s ype, (iii)
p∈P i acy
, which
p o ides he le el o p i acy, (i )
∈Value
is he alue o he en i y i sel , wi h a
s uc u e which will depend on he en i y’s ype, and ( ) a imes amp
s ∈T ime
,
which allows eco ding he ime when he uple is added o he i ual p o ile. We
will deno e by T he se o uples, and by P he se o i ual p o iles.
The complexi y o i ual p o iles depends on he se s
Name
,
Type
,
P i acy
,
Value
, and
Time
. These en i ies a e s uc u ed in nes ed sec ions o he secu e
and co ec unc ioning o he p o ile. Al hough he model does no depend
on how hese pa icula domains a e de ined, we conside a common minimum
s uc u e o p ede ined en i ies which a e cha ac e ized as ollows:
Pe sonal
I consis s in pe sonal and con ac in o ma ion o he use (
pe sonal ∈
Name
); he de aul p i acy is
p i a e ∈P i acy
, al hough i can be o e -
w i en in each a ibu e o allow accessing i o amily o iends, o in-
s ance. Basically, i con ains a collec ion o en i y iden i ie s like
name
,
phone
,
add ess, o email wi h he co esponding in o ma ion.
Rela ions
I p o ides in o ma ion on how use s a e ela ed o each o he (
ela ion ∈
Name
), such ha alues includes en i y names like
amily
,
iends
,
colleagues
,
o
acquain ances
. These nes ed en i ies a e collec ions o use (pe sonal)
in o ma ion wi h in o ma ion abou loca ion, social p o iles and hei ce i i-
ca e hash inge p in . The de aul p i acy le el o hese en i ies is
p i a e ∈
P i acy.
Places
I de ines in o ma ion in a p o ile conce ning loca ions (
place ∈Name
):
home, place o wo k, known places o o he places. Thus, cons an s like
home
o
wo k
belong o he
Name
se in he alue o his en i y. Thei de aul
p i acy le el is us ed.
A i ual p o ile can be accessed and/o modi ied by means o p ocesses
execu ing app op ia e ac ions. In o de o o malize his idea, we a e inspi ed by
Linda [
4
], a coo dina ion language [
7
] consis ing o a se o in e -agen communi-
ca ion p imi i es, which can be i ually added o any p og amming language.
P imi i es in Linda allow p ocesses o ead, dele e, and add uples in a sha ed
uple space. Tuple spaces a e a con enien app oach o ep esen i ual p o iles
sha ed by concu en ly unning p ocesses. A i ual p o ile is ep esen ed by a
mul ise o uples encapsula ed in a de ice. Thus, we adop a mul iple uple
space model.
Following o he app oaches [
3
,
12
], we shall conside a p ocess algeb a
L
includ-
ing he Linda communica ion p imi i es and he usual concu ency connec i es,
pa allel and non-de e minis ic choice. The p imi i es pe mi o add a uple (ou ),
o emo e a uple (in), and o check he p esence (o absence) o a uple ( d,
n d) in a gi en p o ile ( uple space).
P ocesses in
L
p o ide a con enien way o model sc ip s which can be
downloaded om a se e and un on a sma de ice. Thus, he syn ax o
L
is
o mally de ined as ollows:
S∈ L ::= 0 |α.S |S+S|SkS|S(˜
)
α∈Ac ::= d( )|n d( )|in( )|ou (d, )
whe e 0 deno es he emp y p ocess,
d∈D
a de ice iden i ie , and
deno es a
uple. The p ocess
S
(
˜
) deno es a p ocedu e call whe e he p ocedu e de ini ion
will be gi en by a sc ip empla e
S
(
˜x
) (whe e
˜x
is a sequence o a iables
ins an ia ed by a sequence o uples
˜
). In o de o simpli y he de ini ion o
ules modelling he
L
p imi i e ac ions in Subsec ion 4.2, we will assume ha
eading a uple do no imply he e alua ion o usual ope a ions (e.g. a i hme ic
ope a ions) no he a iable ins an ia ion as usual in Linda-based languages. This
assump ion does no imply any loss o gene ali y o he p oposal.
No ice ha we conside p imi i es o locally accessing, adding, and emo ing
uples o a uple space (i.e. a i ual p o ile). Al hough we could ha e also
conside ed accessing and dele ing uples om emo e uple spaces, o ou pu poses
we only need o add uples emo ely. Fo his eason, only he
ou
p imi i e
includes as a pa ame e he de ice on which adding he uple. Tha is,
d
,
in
and
n d
ac ions will be made locally, on he same de ice whe e he sc ip is being
un. The same conside a ions we e made in [
12
]. As i will be shown la e , emo e
adding o uples will only a ec o he a i ac whe e he sc ip was downloaded
om, hus we will no allow a bi a y emo e adding o uples. This asymme ic
ea men o ou and ead p imi i es a e p ecisely one o he ea u es de o ed
by he PeaaS model: local accessing is only made by de ice owne s, and emo e
changes can only be made on a i ac s p o iding he sc ip s o be un.
In ou amewo k, we dis inguish wo kinds o a i ac s: sma de ices and
sma hings. The di e ence be ween hem is ha sma de ices exhibi compu ing
capabili ies, and he e o e hey can download and execu e sc ip s, whe eas sma
hings only p o ide a (link o a) sc ip .
Fo mally, we de ine an a i ac as a pai consis ing o a i ual p o ile and
a p ocess co esponding o he execu ion o one o se e al sc ip s. We assume
ha
D
is a se o a i ac iden i ie s. E e y a i ac
d
also has associa ed a sc ip

de ini ion
Sd
(
˜x
) which can be downloaded by o he a i ac s wi h compu ing
capabili ies (i.e. sma de ices).
De ini ion 2.
An a i ac
d∈D
is cha ac e ized by a pai
hP
:
Sid
, including
a i ual p o ile
P
and a p ocess
S∈ L
, co esponding o he unning sc ip s on
he a i ac . In addi ion, an a i ac can con ain a sc ip de ini ion
Sd
(
˜x
). We
will deno e by
Sd
(
P
) he sc ip ins an ia ed by he speci ic uples in he p o ile
P
.
And we will ep esen by D=P × L × D he se o a i ac s.
A sma hing will be cha ac e ized by ha ing only a p o ile; ha is, i s
p ocess is always he emp y p ocess 0. A ypical example o sma hing would be
a beacon b oadcas ing a Blue oo h Low Ene gy (BLE) signal which encodes he
URL o a sc ip ile o be downloaded om a se e . On he o he hand, ypical
sma de ices a e sma phones, able s, o any o he de ice wi h compu ing
capabili ies. Bo h kinds o a i ac s —sma hings and sma de ices— s o e
in o ma ion in a i ual p o ile.
3.2 Secu i y in Digi al A a a s
The ac ions execu ed o e he i ual p o ile o a sma de ice may eme ge om
in e nal p ocesses o he de ice, o hey may be pa o a sc ip downloaded
om ano he a i ac (e.g. a beacon b oadcas ing a link o a sc ip ile) when
se e al condi ions a e ul illed: he sma de ice is close enough o he beacon,
he beacon a i ac is egis e ed, i s sc ip code is us ed, e c.
In o de o a oid unning un us ed sc ip s, we assume a Ce i ica ion Au ho -
i y capable o ensu e he us ulness o an a i ac
d
, and a Boolean mapping
ce i y
which p o ides his in o ma ion in such a way ha
ce i y
(
d
) is ue when
he emi e o dhas been au hen ica ed.
In addi ion, he ou p imi i e conside ed in he p e ious sec ion allows adding
uples o bo h local and emo e i ual p o iles. Al hough he model imposes
no limi a ions on which p o iles can be emo ely modi ied, he a i ac iden i ie
d
used in a emo e ou (d, ) in a sc ip
Sd
(
˜x
) can only be ha o he a i ac
d
i sel . Thus, an a i ac ’s p o ile may only be emo ely modi ied by unning a
sc ip downloaded om his same a i ac .
Hence, in o de o gua an ee ha he ac ions execu ed while unning a sc ip
on a sma de ice a e secu e, we assume a Boolean mapping
accep
:
Ac × P →
{ ue, alse}
ha es ic s which p imi i es a e enabled, in such a way ha
accep (α, P ) is ue when he ac ion αis accep able on he p o ile P.
Howe e , using ce i ica es and es ic ing emo e addi ion o uples is no
enough o ensu e a co ec in e ac ion be ween sou ce and a ge a i ac s, and
we also need o conside some echnical issues. Indeed, whe eas
ce i y
p o ides
a hi d-pa y decla a ion abou he us o an a i ac , and
accep
con ols wha
ac ions a e pe mi ed inside an a i ac once he sc ip has been downloaded, we
need a way o de ec when wo a i ac s a e ac ually able o communica e wi h
each o he . Fo ins ance, conside a scena io whe e a sma phone ( ep esen ed by
a i ual p o ile
P
) app oaches a sma hing
d
which p o ides a sc ip
Sd
(
˜x
). Fo
downloading he sc ip om
d
and unning i in he sma phone, we assume a
mapping
links
:
P ×D→
2
T
, which p o ides a link o connec o he sma hing,
depending on he a ailabili y o download, he closeness be ween bo h a i ac s,
good signal s eng h, e c. This mapping e u ns a se o uples ep esen ing links
(e.g., a URI o a blue oo h connec ion) p o iding a way o access he a i ac
d
. I he e a e no links, o he p o ile
P
does no accep downloading he sc ip
o e ed by d,links(P, d) will be he emp y se .
No ice ha all he no ions in oduced in his subsec ion (accep ,ce i y, and
links) a e applica ion speci ic, in such a way ha hei pa icula de ini ions will
depend on he applica ion domain and con ex whe e ou amewo k is applied
o.
4 Fo mal amewo k
Now ha we ha e de ined he main elemen s and concep s o ou amewo k, we
can o malize he in e ac ions be ween a i ac s by means o a ansi ion sys em
wi h in-de ice and emo e ope a ions. Then, we show how some in e es ing
p ope ies like bisimila i y and cong uence a e accomplished by he model.
4.1 In-de ice ansi ion sys em
The ope a ional seman ics o
L
is modeled by he ollowing labelled ansi ion
sys em: ·
−→⊆ D × Λ× D
de ined by he ules
1
o Table 1, whe e
D
=
P × L × D
and
Λ
=
{ , ,
:
∈
T}∪{τ}.
Rule Ou
1
desc ibes how he ou pu ope a ion p oceeds as an in e nal mo e
( ep esen ed by label
τ
) which adds he uple
o he p o ile
P
(comma is used
o ep esen he mul ise union). Rule Ou
2
shows ha a uple
is eady o
o e i sel o he a i ac /de ice by pe o ming an ac ion labelled
. Rules In and
Read desc ibe he beha io o he p e ixes
in
(
) and
d
(
) whose labels a e
and
, espec i ely. Rule NRead desc ibes he p e ix ac ion
n d
(
), which p oceeds
when
is no in he p o ile
P
; he ansi ion is labelled wi h
¬
. All hese ules
need ha he cu en de ice’s p o ile accep s he co esponding ac ion. I is wo h
no ing ha we do no include any kind o e alua ion no a iable ins an ia ion
when eading uples, as i is usually made in Linda- ela ed ansi ion ules. This
is only o simplici y easons wi hou loss o gene ali y.
Rule Sum is he s anda d ule o choice composi ion. Rule Sync
1
is he
s anda d ule o he synch oniza ion be ween he complemen a y ac ions
and
.
I models he e ec i e execu ion o an
d
(
) ope a ion. No ice ha he esul ing
p o ile is le unchanged, since he ead ope a ion
d
(
) does no modi y i . Rule
Sync
2
de ines he synch oniza ion be ween wo p ocesses pe o ming ansi ions
labelled wi h
and
, espec i ely. I models he e ec i e execu ion o
in
(
)
1Fo he sake o simplici y we will conside only ini e p ocesses he e.
ac ion. The usual ule Pa
1
o he pa allel ope a o can be applied o any label.
The ansi ion sys em is conside ed closed w. . . commu a i e and associa i e
p ope ies o sum (+) and pa allel (k) ope a o s.
(Ou 1)accep (ou (d, ), P )
hP:ou (d, ).Sid
τ
−→ hP, :Sid
(Ou 2)hP, :Sid
¯
−→ hP:Sid
(Read)accep ( d( ), P )
hP: d( ).Sid
−→ hP:Sid
(In)accep (in( ), P )
hP:in( ).Sid
−→ hP:Sid
(NRead) 6∈ P∧accep (n d( ), P )
hP:n d( ).Sid
¬
−→ hP:Sid
(Sum)hP:S1id
α
−→ hP0:S0
1id
hP:S1+S2id
α
−→ hP0:S0
1+S2id
(Sync1)hP:S1id
−→ hP:S0
1idhP:S2id
−→ hP0:S2id
hP:S1kS2id
τ
−→ hP:S0
1kS2id
(Sync2)hP:S1id
−→ hP:S0
1idhP:S2id
−→ hP0:S2id
hP:S1kS2id
τ
−→ hP0:S0
1kS2id
(Pa 1)hP:S1id
α
−→ hP0:S0
1id
hP:S1kS2id
α
−→ hP0:S0
1kS2id
Table 1. T ansi ion sys em o sma de ices
No ice ha ac ion
ou
(
d,
) is only conside ed in Table 1 when i is unning
in he de ice
d
. I s ull beha io ( emo e adding o uples) will be de ined when
he in e ac ion among de ices is exp essed in Table 2.
4.2 Remo e ansi ion sys em
In o de o de ine how a i ac s in e ac , we conside con igu a ions composed o
a pa allel composi ion o a i ac s as ollows:
hP1:S1id1| hP2:S2id2| · · · | hPn:Snidn
whe e
Pi
(
i
= 1
..n
) a e i ual p o iles o a i ac s —ei he sma de ices and
sma hings—,
Si
a e sc ip s unning in sma de ices, and
di
ep esen he
de ice iden i ie s. No ice ha we deno e in a di e en way he pa allel composi ion
o a i ac s (
|
) and he pa allel composi ion o p ocesses inside a sma de ice (
k
).
The ansi ion sys em
·
−→
de ined in Table 1 is ex ended o con igu a ions
by he in e ence ules gi en in Table 2.
(Remo e)accep (ou (e, ), Q)
hP:ou (e, ).Sid| hQ:Tie
τ
−→ hP:Sid| hQ, :Tie
(Sync3)ce i y(e)∧b∈links(P, e)
hP:Sid| hQ:Tie
τ
−→ hP, b :SkSe(b, Q)id| hQ:Tie
(Pa 2)D1
α
−→ D0
1
D1|D2
α
−→ D0
1|D2
Table 2. T ansi ion sys em
Rule Remo e models emo e ac ions modi ying he i ual p o ile which
belongs o he sma hing om which he sc ip being un was downloaded. We
conside his ansi ion as a silen s ep om an obse a ional poin o iew. Fo
his eason, we use he label τ.
Rule Sync
3
ep esen s he in e ac ion be ween wo a i ac s ( ypically, a sma
de ice and a sma hing). In his case, he sc ip associa ed wi h a sma hing
e
, p e iously ce i ied, is downloaded h ough a link
b
es ablishing a connec ion
be ween he i ual p o ile
P
and
e
. Thus, he sc ip o be execu ed in he con ex
o he sma de ice
d
(in pa allel wi h o he possible pending p ocesses) will be
Se
(
b, Q
) (such as i was de ined in De ini ion 2). No ice ha , in his case, he
sc ip is ins an ia ed no only by he p o ile
Q
bu also by he link
b
. This allows
cus omizing he sc ip o he a i ac which p o ides access o i . In addi ion, he
link uple
b
is added o he p o ile
P
, so eco ding ha he sma hing has been
al eady “ isi ed”.
Rule Pa
2
desc ibes he way in which he pa allel composi ion o a i ac s
p oceeds. No e ha he pa allel composi ion o p ocesses inside a sma de ice is
modelled by Rule Pa
1
in Table 1. Ac ually, any in e ac ion in he con ex o a
sma de ice is go e ned by ules in ha able.
We conside he ansi ion sys em closed w. . . usual s uc u al cong uence
(commu a i e and associa i e p ope ies) o bo h pa allel connec o s.
The ules in Table 1 and Table 2 a e used o de ine he se o de i a ions in
an en i onmen whe e sma de ices and sma hings a e in e ac ing wi h each
o he . Following [
3
], bo h educ ions labelled
τ
and educ ions labelled
¬
a e
conside ed. Fo mally, his co esponds o in oducing he ollowing de i a ion
3.
Nadia Busi, Robe o Go ie i, and Gianluigi Za a a o. On he Tu ing equi alence
o Linda coo dina ion p imi i es. Elec . No es Theo . Compu . Sci., 7:75, 1997.
4.
Nicholas Ca ie o and Da id Gele n e . Linda in con ex . Commun. ACM, 32(4):444–
458, Ap il 1989.
5.
R. De Nicola, G. L. Fe a i, and R. Pugliese. Klaim: a ke nel language o agen s
in e ac ion and mobili y. IEEE T ansac ions on So wa e Enginee ing, 24(5):315–
330, May 1998.
6.
Rocco De Nicola, Diego La ella, Albe o Lluch La uen e, Michele Lo e i, And ea
Ma ghe i, Mieke Massink, And ea Mo iche a, Rosa io Pugliese, F ancesco Tiezzi,
and And ea Vandin. The SCEL Language: Design, Implemen a ion, Ve i ica ion,
pages 3–71. Sp inge In e na ional Publishing, Cham, 2015.
7.
Da id Gele n e and Nicholas Ca ie o. Coo dina ion languages and hei signi i-
cance. Commun. ACM, 35(2):96–, Feb ua y 1992.
8.
To -Mo en G ønli, Gheo ghi a Ghinea, and Muhammad Younas. Con ex -awa e
and au oma ic con igu a ion o mobile de ices in cloud-enabled ubiqui ous compu -
ing. Pe sonal and ubiqui ous compu ing, 18(4):883–894, 2014.
9.
Jaya a dhana Gubbi, Rajkuma Buyya, Sla en Ma usic, and Ma imu hu
Palaniswami. In e ne o Things (IoT): A ision, a chi ec u al elemen s, and
u u e di ec ions. Fu u e gene a ion compu e sys ems, 29(7):1645–1660, 2013.
10.
Joaquin Guillen, Ja ie Mi anda, Ja ie Be ocal, Jose Ga cia-Alonso, Juan Manuel
Mu illo, and Ca los Canal. People as a Se ice: a mobile-cen ic model o p o iding
collec i e sociological p o iles. IEEE so wa e, 31(2):48–53, 2014.
11.
Dominique Guina d, Vlad T i a, F iedemann Ma e n, and E ik Wilde. F om he
In e ne o Things o he Web o Things: Resou ce-o ien ed a chi ec u e and bes
p ac ices. In A chi ec ing he In e ne o Things, pages 97–129. Sp inge , 2011.
12.
Ronaldo Menezes, And ea Omicini, and Mi ko Vi oli. On he seman ics o coo di-
na ion models o dis ibu ed sys ems: The LogOp case s udy. In Founda ions o
Coo dina ion Languages and So wa e A chi ec u e (FOCLASA 2003), olume 97
o Elec onic No es in Theo e ical Compu e Science, pages 97–124. Else ie , 2004.
13.
Alejand o P´e ez-Ve eda, Daniel Flo es-Ma ´ın, Ca los Canal, and Juan M Mu illo.
Towa ds dynamically p og ammable de ices using beacons. In In e na ional Con-
e ence on Web Enginee ing, olume 11153 o LNCS, pages 49–58. Sp inge , 2018.
14.
Gian Pie o Picco, Amy L. Mu phy, and G uia-Ca alin Roman. Lime: Linda
mee s mobili y. In P oceedings o he 21s In e na ional Con e ence on So wa e
Enginee ing, ICSE ’99, pages 368–377. ACM, 1999.
15.
Mika Raen o, An i Oulas i a, and Na han Eagle. Sma phones: An eme ging ool
o social scien is s. Sociological me hods & esea ch, 37(3):426–454, 2009.
16.
Jo ge Sa Sil a, Pei Zhang, T e o Pe ing, Fe nando Boa ida, Takahi o Ha a, and
Nicolas C Liebau. People-cen ic In e ne o Things. IEEE Communica ions
Magazine, 55(2):18–19, 2017.
17.
An e o Tai alsaa i and Tommi Mikkonen. A oadmap o he p og ammable wo ld:
so wa e challenges in he IoT e a. IEEE So wa e, 34(1):72–80, 2017.
18.
Fei-Yue Wang, Ka hleen M Ca ley, Daniel Zeng, and Wenji Mao. Social compu ing:
F om social in o ma ics o social in elligence. IEEE In elligen sys ems, 22(2), 2007.
19.
Yu eng Wang, A hanasios V. Vasilakos, Qun Jin, and Jianhua Ma. Su ey on mobile
social ne wo king in p oximi y (MSNP): app oaches, challenges and a chi ec u e.
Wi eless ne wo ks, 20(6):1295–1311, 2014.
20.
Wan-Shiou Yang and San-Yih Hwang. iT a el: A ecommende sys em in mobile
pee - o-pee en i onmen . Jou nal o Sys ems and So wa e, 86(1):12–20, 2013.