In recent years, event-driven programming languages, e.g. those based on Event Condition Action (ECA) rules, have emerged as a promising paradigm for implementing smart systems, such as IoT devices. Still, actual implementations are bound to a centralized infrastructure, limiting scalability and security. In this work, we present attribute-based memory updates (AbU), a new interaction mechanism aiming to extend the ECA programming paradigm to distributed systems. It relies on attribute-based communication, that is similar to broadcast, but receivers are selected “on the fly” by means of predicates over their attributes. With AbU, smart devices can be easily programmed via ECA rules and, at the same time, they can be deployed to a distributed network. Hence, a centralized infrastructure is not needed anymore: the computation is moved on the edge, improving reliability, scalability, privacy and security.
are managed by a central coordinator node (often deployed on the cloud). This leads to several issues: scalability (as the IoT devices will increase exponentially), availability (what happens when the central node is not reachable?) and privacy (users’ data are continuously sent to remote, unknown, servers, not under user’s control). Thus, in these situations we may prefer to move computation closer to the edge of the network, akin fog computing: the ECA rules should be stored and executed directly on the nodes, in a truly distributed setting. This approach reduces data transfers between the edge and the center of the network—in fact, there can be no center at all, thus increasing scalability and resilience—but, on the other hand, it requires a distributed coordination and communication of these components.
To mitigate these issues, we introduce AbU (for “Attribute-based Updates”), a new calculus
aiming at merging the simplicity of ECA programming with distributed coordination
mechanisms in the spirit of attribute-based communication (AbC) [
Integrating attribute-based communication in the ECA paradigm is not obvious, since the ifrst adopts a message-passing mechanism while the latter uses memory-based events. To solve the problem, in AbU attribute-based communication is reduced to events of the same kind ECA programs already deal with, that is, memory updates. For instance, the following AbU rule @( = logger) : ← + means “when (my local) variable changes, add its value to the variable of all nodes whose variable has value logger”. Clearly, the update of may trigger other rules on these (remote) nodes, and so on. We call this mechanism attribute-based memory updates, since it can be seen as the memory-based counterpart of attribute-based message-passing.
This smooth integration of paradigms makes it easier to extend to the distributed setting known results and techniques. As an example, we will provide a simple syntactic check to guarantee stabilization, i.e., that a chain of rule executions triggered by an external event will eventually terminate.
AbU is a calculus following the Event Condition Action paradigm, augmented with attributebased communication. This solution embodies the programming simplicity of ECA rules, but it is expressive enough to model complex coordination scenarios, typical of distributed systems.
In AbU, a smart device is modeled by a node ⟨Σ, Θ⟩. is a list of ECA rules of the form evt ⋗ task, where evt is the event and task is the task. The latter is a pair cnd : act, where cnd is the condition and act is the action. The full syntax of AbU ECA rules is depicted in Fig. 1. The configuration of the node is given by a state Σ, mapping resources to values, and an execution pool Θ, which is a set of memory updates. An update is a finite list of pairs (, ), meaning rule ::= evt ⋗ task evt ::= | evt evt act ::= | ← act | ← act task ::= cnd : act ::= ⊥ | ⊤ | ¬ | ∧ | ∨ | ◁▷ ::= | | | ⊗ ∈ X ∈ V that the resource will take the value after the execution of the update. When one of the resources in a rule event is modified, the rule is fired and its task evaluated. Evaluation does not change the resource states immediately; instead, it yields update operations that are added to the execution pools, and applied later on.
A task condition is a boolean expression, optionally prefixed with the task is local; otherwise the task is remote. In local tasks, the condition is checked in the local node and, if it holds, the action is evaluated. For remote tasks, the action is evaluated on every node where the condition holds. An action is a finite list of assignments of value expressions to local or remote . The evaluation of an action yields an update, which is added to the node pool of the local or remote nodes, in the case of local or remote tasks, respectively. As an one for each smart device to model. of every other node”. Finally, an AbU system S is just the parallel composition of AbU nodes, + means “add the value of the current node to the
The behavior of an AbU system is specified by means of (small-step) semantics, modeled as a
labeled transition system (LTS) S1 − _ S2. The semantics is distributed, in the sense that each
node does not have a global knowledge about the system. In the AbU semantics, that can be
found in the original paper [
Consider the scenario sketched in the introduction, where an “access” node aims at sending its local access time to all “logger” nodes in the system. In other words, this node is activated when changes, i.e., when a user performs access. Suppose that the node, together with the time-stamp, aims at sending the IP address of the user and the name of the accessed resource. On the other side, the logger nodes record the access time, the IP address and the resource name. Furthermore, these nodes contain a black-list of IP addresses. A logger node noticing an access from a black-listed IP is in charge of notifying an intrusion detection system (IDS). The system is formalized in AbU as follows, supposing to have two access and two logger nodes.
S1 ≜ ⟨Σ1, ∅⟩ = ⟨[ ↦→ ↦→ 00 : 00 : 00 ↦→ camera], ∅⟩ S2 ≜ ⟨Σ2, ∅⟩ = ⟨[ ↦→ ↦→ 00 : 00 : 00 ↦→ lock], ∅⟩ S3 ≜ ⟨Σ3, ∅⟩ = ⟨[ ↦→ logger ↦→ ↦→ ↦→ ], ∅⟩ S4 ≜ ⟨Σ4, ∅⟩ = ⟨[ ↦→ logger ↦→ ↦→ 167.123.23.2; ↦→ ], ∅⟩ ≜ ⋗ @( = logger) : ←
append | ; ; | ≜ ⋗ (tail[]. ∈ ) : ←
tail[] At the beginning, in the AbU system S1 ‖ S2 ‖ S3 ‖ S4 all pools are empty, so there is nothing to compute. At some point, an access is made on the resource camera, so the rule (Input) is applied on S1, namely ⟨Σ1, ∅⟩− − ▶_ ⟨Σ′1, ∅⟩, where Σ′1 = [ ↦→ 15 : 07 : 00 ↦→ camera ↦→ 167.123.23.2] and = @( = logger) : ← aopthpeernndodes.|1I6n7p.1a2rt3i.c2u3l.a2r;, 1w5e:h0a7v:e0:0;c⟨aΣm2e,r∅a|⟩. − _Now,⟨aΣd2i,sc∅o⟩v,ery⟨Σph3a,s∅e⟩is−_perfo⟨rΣm3e,Θd⟩o,nanaldl ⟨Σ4, ∅⟩ − _ ⟨Σ4, Θ⟩. Here, the pool Θ is {(, |167.123.23.2; 15 : 07 : 00; camera|)}.
Now, the third and the fourth nodes can apply an execution step, since their pools are not ▷ ⟨Σ′3, ∅⟩, by applyempty. Suppose the third node is chosen, namely we have ⟨Σ3, Θ⟩ − _ ing the rule (Exec), and Σ′3 = [ ↦→ logger ↦→ |167.123.23.2; 15 : 07 : 00; camera| ↦→ ∅ ↦→ ]. Note that, in this case, no rule is triggered by the executed update. Since there is nothing to discover, all the other nodes do not have to update their pool. Finally, the ▷ ⟨Σ′4, Θ′⟩, by applying the fourth node can execute, namely we have that ⟨Σ4, Θ⟩ − _ rule (Exec). Here, Σ′4 = [ ↦→ logger ↦→ |167.123.23.2; 15 : 07 : 00; camera| ↦→ 167.123.23.2; ↦→ ] and Θ′ = {(, |167.123.23.2; 15 : 07 : 00; camera|)}. In this case, the execution of the update triggers a rule of the node but the rule is local so, also in this case, the discovery phase does not have efect. Since all pools are empty, the execution stops, until a new input (i.e., an external change to resources) is performed.
An AbU system S is stable, when no more execution steps can be performed, namely when all execution pools of all nodes in S are empty. In the case of a stable system, only the rule (Input) can be applied, i.e., an external environment change is needed to (re)start the computation.
We can define a (big-step) semantics S ⇝ S′ between stable systems, dubbed wave semantics,
in terms of the small-step semantics of AbU (see again the original paper [
The wave semantics (and, hence, an AbU system) may exhibit internal divergence: once an input step starts the computation, the subsequent execution steps may not reach a stable system, even if intermediate inputs are not performed. In order to prevent this situation, we define a simple syntactic condition on the ECA rules, that guarantees (internal) termination. Each system satisfying the condition eventually becomes stable, after an initial input and without further interleaving inputs. The idea is to build an ECA dependency graph expressing dependencies between the resources handled by an AbU system: a resources in the graph is linked to another resource in the graph when a change of may potentially afect the value of .
To build such graph we need: the output resources of an ECA rule, namely the resources involved in the actions performed by the rule (they are given by the resources assigned in the rule task); and the input resources of an ECA rule, namely the resources that the rule depends on (they are the resources in the rule event). Then, the ECA dependency graph of a system S is a directed graph (, ) where nodes are the input and output resources of all ECA rules in S, while the edges link two resources and if is an input resource of a rule in S and is an output resource of the same rule. Indeed, this means that is potentially assigned by a rule in S when is changed. The suficient syntactic condition for the termination of the wave semantics (i.e., stabilization) consists in the acyclicity of the ECA dependency graph. Proposition 1 (Stabilization). Given an AbU system S, if the ECA dependency graph (, ) of S is acyclic, then there exists a system S′ such that S ⇝ S′.
A simple mechanism enforcing termination consists in computing the transitive closure + of and to check if it contains reflexive pairs, i.e., elements of the form (, ), for a resource . If there are no reflexive pairs then the graph is acyclic and stabilization is fulfilled.
In this paper we have presented AbU, a new calculus merging the simplicity of ECA programming
with attribute-based memory updates. This provides us an efective method for programming
IoT smart devices in a fully-distributed setting, without sacrificing the simplicity typical of ECA
rules. Moreover, AbU can be used as a solid foundational model for edge computation.
Future work First, we are interested in porting to AbU the verification techniques developed
for other ECA languages [