Abstract Internet of things (IoT) applications called SmartApps are event‐driven programs running on the SmartThings cloud. To understand the behaviour of SmartApps, users may have questions regarding which execution flows follow particular events or why specific actions occur. However, checking internal programme behaviours, such as event‐driven execution flows, is more difficult for users because SmartApps run on the cloud. In this paper, we propose SmartProvenance, which is a provenance system for IoT applications and provides a graphical user interface (GUI) environment for provenance queries on event flow graphs. The event flow graph of a SmartApp visualises all execution control flows initiated by events, which are constructed by performing static programme analysis. The graph is decorated with dynamically collected event and action information in the GUI interface for provenance queries. Then, users can query the provenance by simply clicking on the graph. An event flow graph as the form of a GUI for queries in the SmartProvenance system allows users to view IoT services by all possible event flow paths in a SmartApp. Thus, the provenance information being visualised on the event flow graph can be intuitively understood in the context of IoT services. Therefore, users can answer provenance questions themselves without difficulty.

The polymorphic RPC calculus allows programmers to write succinct multitier programs using polymorphic location constructs. However, until now it lacked an implementation. We develop an experimental programming language based on the polymorphic RPC calculus. We introduce a polymorphic Client-Server (CS) calculus with the client and server parts separated. In contrast to existing untyped CS calculi, our calculus is not only able to resolve polymorphic locations statically, but it is also able to do so dynamically. We design a type-based slicing compilation of the polymorphic RPC calculus into this CS calculus, proving type and semantic correctness. We propose a method to erase types unnecessary for execution but retaining locations at runtime by translating the polymorphic CS calculus into an untyped CS calculus, proving semantic correctness.

SmartThings is one of the most widely used smart home platforms for the internet of things (IoT). SmartApps are IoT applications on the SmartThings platform that enables automation of home devices. SmartApps are event‐driven; inputs are received from device events, and outputs are issued to control devices. Understanding the behaviour of IoT applications is a challenge because the inputs and outputs are rarely visible. To tackle the challenge, the proposed approach is to visualise IoT applications as a set of IoT services. The authors propose an event‐flow‐based visualisation method where a flow from an event to action is viewed as an IoT service. The authors implement a tool called SmartVisual that performs a static analysis on SmartApps to generate a diagram of event flows. The tool also provides a tree model of the static structure of SmartApps and software metrics relevant to the event‐driven nature. The tool was applied to 64 SmartApp samples provided by SmartThings. Each SmartApp had four event flows on average, although the most complex SmartApp had 58 event flows, and two inputs and two outputs, and the average length of the event flows was 1.43 methods.

Abstract With multi-tier programming languages, programmers can specify the locations of code to run in order to reduce development efforts for the web-based client–server model where programmers write client and server programs separately and test the multiple programs together. The RPC calculus, one of the foundations of those languages by Cooper and Wadler, has the feature of symmetric communication in programmer’s writing arbitrarily deep nested client–server interactions. The feature of the calculus is fully implemented by asymmetric communication in trampolined style suitable for the client–server model. However, the existing research only considers a stateless server strategy in which all server states are encoded for transmission to the client so that server states do not need to be stored in the server. It cannot always correctly handle all stateful operations involving disks or databases. To resolve this problem, we first propose new stateful calculi that fully support both symmetric communication from the programmer’s viewpoint and asymmetric communication in its implementation using trampolined style. All the existing calculi either provide only the feature of asymmetric communication or propose only symmetric implementation suitable for the peer-to-peer model, rather than the client–server model. Second, the method used to design our stateful server strategy is based on a new locative type system which paves the way for a theory of RPC calculi for the client–server model. Besides proposing the new stateful calculi, this theory can improve the existing stateless server strategy to construct new state-encoding calculi that eliminate runtime checks on remote procedure calls present in the existing strategy, and it enables us to design a new mixed strategy that combines the benefits of both kinds of strategies. As far as we know, there are no typed multi-tier calculi that offer programmers the feature of symmetric communication with the implementation of asymmetric communication under the three strategies together.

In this paper, we first propose a visual block language Smart Block for IoT, especially for SmartThings. We also developed a visual programming environment for Smart Block so that users can write their own SmartApps in this language easily, even though they are not expert programmers. We designed the language based on IoTa calculus, a core calculus for Internet of Things Automation that generalizes Event-Condition-Action (ECA) rules for home automation. We implemented a visual programming environment for Smart Block with Blockly, a client-side JavaScript library for creating visual block languages.