Distributed Programming of Smart Systems with Event-Condition-Action Rules (Short Paper)⋆ Marino Miculan1,2 , Michele Pasqua3 1 University of Udine, Italy 2 Ca’ Foscari University of Venice, Italy 3 University of Verona, Italy Abstract 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. Keywords ECA rules, Attribute-based communication systems, Formal methods, Autonomic computing 1. Introduction Event Condition Action (ECA) languages are an intuitive and powerful paradigm for program- ming reactive systems. In the ECA programming paradigm, the behaviour of a system is defined by a set of rules of the form “on Event if Condition do Action” which means: when Event occurs, if Condition is verified then execute Action. This paradigm is particularly suited for programming smart systems, such as in IoT scenarios [2, 3, 4]: ECA systems react to inputs (as events) from the environment performing internal actions (updating the node local memory) and external actions, which influence the environment itself. Indeed, all main platforms in the field of Home/Automotive IoT (e.g., IFTTT, Samsung SmartThings, Microsoft PowerAutomate, Zapier, etc.) adopt this programming style. Despite this simplicity, actual ECA platforms adopt a centralized infrastructure: IoT devices Proceedings of the 23rd Italian Conference on Theoretical Computer Science, Rome, Italy, September 7-9, 2022 ⋆ This is an short version of the paper that we presented at ICTAC 2021 [1]. Work supported by the Italian MIUR project PRIN 2017FTXR7S IT MATTERS (Methods and Tools for Trustworthy Smart Systems). " marino.miculan@uniud.it (M. Miculan); michele.pasqua@univr.it (M. Pasqua) ~ https://users.dimi.uniud.it/~marino.miculan/ (M. Miculan); https://michelepasqua.github.io/ (M. Pasqua)  0000-0003-0755-3444 (M. Miculan); 0000-0002-9475-4836 (M. Pasqua) © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) 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 mecha- nisms in the spirit of attribute-based communication (AbC) [5]. Attribute-based communication is a time-coupled, space-uncoupled interaction model recently introduced for coordinating large numbers of components. The key aspect of attribute-based communication is that the actual receivers are selected “on the fly” by means of predicates. Integrating attribute-based communication in the ECA paradigm is not obvious, since the first 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. 2. Attribute-based Memory Updates AbU is a calculus following the Event Condition Action paradigm, augmented with attribute- based communication. This solution embodies the programming simplicity of ECA rules, but it is expressive enough to model complex coordination scenarios, typical of distributed systems. 2.1. Syntax and Semantics 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 cnd ::= 𝜙 | @𝜙 evt ::= 𝑥 | evt evt 𝜙 ::= ⊥ | ⊤ | ¬𝜙 | 𝜙 ∧ 𝜙 | 𝜙 ∨ 𝜙 | 𝜀 ◁▷ 𝜀 act ::= 𝜖 | 𝑥 ← 𝜀 act | 𝑥 ← 𝜀 act 𝜀 ::= 𝑣 | 𝑥 | 𝑥 | 𝜀 ⊗ 𝜀 task ::= cnd : act 𝑥∈X 𝑣∈V Figure 1: AbU syntax for ECA rules. 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 @: when @ is not present, 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 example, the (remote) task @⊤ : 𝑥 ← 𝑥 + 𝑥 means “add the value of the current node 𝑥 to the 𝑥 of every other node”. Finally, an AbU system S is just the parallel composition of AbU nodes, one for each smart device to model. 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 [1], a rule (Exec) executes an update picked from the pool; while a rule (Input) models an external modification of some resources. The execution of an update, or an external change in the resources, may trigger some rules of the nodes. Hence, after updating a node state, the semantics of a node launches a discovery phase, with the goal of finding new updates to add to the local pool (or some pools of remote nodes), given by the activation of some rules. The discovery phase is composed by two parts. Firstly, a node 𝑅⟨Σ, Θ⟩ performs a local discovery to add to the local pool Θ all updates originated by some rules in 𝑅 that contain local tasks. Then, the node computes a list of remote tasks that may update external nodes and sends it to all nodes in the system. This is modeled with the LTS labels ▷ 𝑇 and ▶ 𝑇 , produced by the rules (Exec) and (Input), respectively. On the other side, when a node receives a list 𝑇 of tasks, executing the rule (Disc) with a LTS label 𝑇 , it evaluates them and adds to its pool the actions generated by the tasks whose condition is satisfied. Finally, the rule (Step) completes (on all nodes in the system) a discovery phase launched by a given node. 2.2. A Working Example 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) : 𝑙𝑜𝑔 ← append 𝑙𝑜𝑔 |167.123.23.2; 15 : 07 : 00; camera|. Now, a discovery phase is performed on all 𝑇 𝑇 other nodes. In particular, we have: 𝑅𝑎 ⟨Σ2 , ∅⟩ − _ 𝑅𝑎 ⟨Σ2 , ∅⟩, 𝑅𝑙 ⟨Σ3 , ∅⟩ −_ 𝑅𝑙 ⟨Σ3 , Θ⟩, and 𝑇 𝑅𝑙 ⟨Σ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 ▷𝜀 empty. Suppose the third node is chosen, namely we have 𝑅𝑙 ⟨Σ3 , Θ⟩ −_ 𝑅𝑙 ⟨Σ′3 , ∅⟩, by apply- 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 ▷𝜀 fourth node can execute, namely we have that 𝑅𝑙 ⟨Σ4 , Θ⟩ −_ 𝑅𝑙 ⟨Σ′4 , Θ′ ⟩, by applying the 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 effect. Since all pools are empty, the execution stops, until a new input (i.e., an external change to resources) is performed. 2.3. Waves and Stabilization 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 [1] for details). The idea is that a (stable) system reacts to an external stimulus by executing a series of tasks (a “wave”), until it becomes stable again, waiting for the next stimulus. Note that, in the wave semantics inputs do not interleave with internal steps: this leaves the system the time to reach stability before the next input. If we allow arbitrary input steps during the computation, a system may never reach stability since the execution pools could be never emptied. This assumption has a practical interpretation: in the IoT context, usually internal computation steps take much less time of changes in the environment, i.e., input from sensors [6]. 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 affect 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 sufficient 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. 3. Conclusions and Future Work 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 effective 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 [7, 8, 9]. Another interesting issue is distributed runtime verification and monitoring, in order to detect violations at runtime of given correctness properties, e.g., expressed in temporal logics like the 𝜇-calculus [10]. Similarly, we can define syntactic criteria and corresponding verification mechanisms to guarantee confluence. Indeed, in practical IoT scenarios, it is important to ensure that the rules execution order does not impact the overall behavior (which is a sort of rule determinism). Along this line, in IoT systems it is often important to guarantee that inputs are processed within precise time bounds; to this end, we can think of adding quantitative aspects to the AbU semantics, following [11]. Finally, a new generalization of attribute-based communication has been presented in [12]; it could be interesting to investigate how to apply that interaction model to the ECA programming. References [1] M. Miculan, M. Pasqua, A calculus for attribute-based memory updates, in: A. Cerone, P. C. Ölveczky (Eds.), Theoretical Aspects of Computing – ICTAC 2021, Springer International Publishing, Cham, 2021, pp. 366–385. doi:10.1007/978-3-030-85315-0\_21. [2] J. Cano, E. Rutten, G. Delaval, Y. Benazzouz, L. Gurgen, ECA rules for IoT environment: A case study in safe design, in: 8th Int. Conf. on Self-Adaptive and Self-Organizing Systems Workshops, IEEE, USA, 2014, pp. 116–121. doi:10.1109/SASOW.2014.32. [3] M. Balliu, M. Merro, M. Pasqua, Securing cross-app interactions in IoT platforms, in: 32nd IEEE Computer Security Foundations Symposium, Hoboken, NJ, USA, IEEE, 2019, pp. 319–334. doi:10.1109/CSF.2019.00029. [4] M. Balliu, M. Merro, M. Pasqua, M. Shcherbakov, Friendly fire: Cross-app interactions in IoT platforms, ACM Trans. Priv. Secur. 24 (2021) 16:1–16:40. doi:10.1145/3444963. [5] Y. Abd Alrahman, R. De Nicola, M. Loreti, F. Tiezzi, R. Vigo, A calculus for attribute-based communication, in: 30th Symposium on Applied Computing, ACM, 2015, pp. 1840–1845. doi:10.1145/2695664.2695668. [6] D. R. Cacciagrano, R. Culmone, IRON: Reliable domain specific language for programming IoT devices, Internet Things 9 (2020) 100020. doi:10.1016/j.iot.2018.09.006. [7] X. Jin, Y. Lembachar, G. Ciardo, Symbolic verification of ECA rules, in: D. Moldt (Ed.), Joint Proceedings of PNSE ’13 and ModBE ’13, Milano, Italy, volume 989, CEUR-WS.org, 2013, pp. 41–59. URL: http://ceur-ws.org/Vol-989/paper17.pdf. [8] C. Vannucchi, M. Diamanti, G. Mazzante, D. R. Cacciagrano, F. Corradini, R. Culmone, N. Gorogiannis, L. Mostarda, F. Raimondi, vIRONy: A tool for analysis and verification of ECA rules in intelligent environments, in: Int. Conf. on Intell. Environ., S. Korea, IEEE, 2017, pp. 92–99. doi:10.1109/IE.2017.32. [9] C. Vannucchi, M. Diamanti, G. Mazzante, D. R. Cacciagrano, R. Culmone, N. Gorogian- nis, L. Mostarda, F. Raimondi, Symbolic verification of event-condition-action rules in intelligent environments, J. Reliab. Intell. Environ. 3 (2017) 117–130. doi:10.1007/ s40860-017-0036-z. [10] M. Miculan, On the formalization of the modal 𝜇-calculus in the Calculus of Inductive Constructions, Inf. Comput. 164 (2001) 199–231. doi:10.1006/inco.2000.2902. [11] M. Miculan, M. Peressotti, Structural operational semantics for non-deterministic processes with quantitative aspects, Theor. Comput. Sci. 655 (2016) 135–154. doi:10.1016/j.tcs. 2016.01.012. [12] M. Miculan, M. Paier, A calculus of subjective communication, in: U. Dal Lago, D. Gorla (Eds.), 23rd Italian Conference on Theoretical Computer Science (ICTCS), Proceedings, CEUR Workshop Proceedings, CEUR-WS.org, 2022, pp. 1–13.