A Tool to Edit and Verify IoT System Architecture Model Shinpei Ogata∗ , Hiroyuki Nakagawa† , Yoshitaka Aoki‡ , Kazuki Kobayashi∗ , Yuko Fukushima‡ ∗ Shinshu University, Nagano, Japan Email: ogata@cs.shinshu-u.ac.jp, kby@shinshu-u.ac.jp † Osaka University, Osaka, Japan Email: nakagawa@ist.osaka-u.ac.jp ‡ Nihon Unisys, Ltd., Tokyo, Japan Email: {yoshitaka.aoki, yuko.fukushima}@unisys.co.jp Abstract—The spread of IoT (Internet of Things) categorized into a corresponding single layer, and widely captures such into a type of cyber-physical system makes future systems larger intra- and inter-relationships between objects. Each type of and more complex than ever. Various components such as cloud relationship has a respective description space called a layer so services, edges, devices and energy suppliers play important roles when constructing an IoT system. Moreover, components in such that the complexity can be mitigated even if many relationships systems have various relationships to other components. Hence, which may be different from each other are defined. A layer a simple and extendable specification notation for grasping such is also placed in an architectural view at an early stage of the relationships is sought for architectural design of IoT systems. development conforming to the twin peaks model. We present When we design such IoT Systems, effective verification also a novel tool which provides two main features for supporting should be provided so that we can identify critical system faults. We present a tool to edit and verify IoT system architecture TORTE: models. The tool extends a UML editor to enable easy editing of • An editor for creating a layered model of an IoT system architectural models, and verifies them using the logic program- architecture using six types of architectural objects and ming language Prolog. relationships. Keywords-IoT, Architectural Model, Logic Programming, Ver- • A verifier for checking the consistency of the model using ification, Twin Peaks Model. logic programming. In this paper, we experimentally model an existing farm I. I NTRODUCTION monitoring system, which is an IoT system, using the tool. IoT systems are often developed as large-scale systems The monitoring system has various physical objects such as a because they have to deal with not only cyberspaces but also camera, solar panel, and battery, and cyber objects such as an physical spaces. Cyberspaces contain cloud services storing original monitoring service and some SNSs (Social Network and utilizing big data, whereas physical spaces contain devices Services). We demonstrate our tool by applying it to the model interacting with things outside of the system and equipment of the monitoring system. supplying energy to other pieces of physical equipment. Therefore, system faults occur frequently in such IoT systems II. D ESIGN M ODEL FOR I OT S YSTEM A RCHITECTURES than ones in traditional software centric systems. Developers Our architectural model consists of a set of six structural should comprehend target IoT systems that contain various diagrams in a variant UML class diagram notation. The model components and their mixed and complicated relationships. also provides six types of architectural objects (hereafter sim- The twin peaks model [1], [2] describes a method to ply called objects) shown in Table I and directed relationships develop software requirements and architectures concurrently (hereafter simply called relationships) shown in Table II. but separately using incremental development. This model is Among these objects, energy suppliers do not often appear still efficient when we construct an IoT system. Goal models in general software design, but play an important role when we [3], [4] and use case models [5] are representative models for consider the sustainability and dependability of IoT systems. requirements analysis. The goal models, such as i* [6], can In particular, when we design an IoT system under unreliable represent actor relationships; the use case models, on the other energy suppliers, the amount of energy consumption and the hand, mainly represent use-case-centric relationships instead lack of energy should be considered. Therefore, we have of actor relationships. We can analyze intentions and features captured energy suppliers as energy objects. Figure 1 shows using goal models and use case models; however, when we de- a model example and the tool. The tool is introduced in detail sign a system architecture, it is difficult to comprehend various in Section IV. Figure 1(a) shows an example of layers re- relationships between cyber objects and physical objects. In garding transmit-data and transmit-energy in the this paper, architectural objects are defined as a super concept farm monitoring system. A rectangle, i.e. class, represents an of components and actors.. object and an arrow, i.e. association, represents a relationship. We propose TORTE, which is a method of modeling IoT A string between << and >>, i.e. stereotype, represents the system architectures. In TORTE, architectural objects, their re- type of object or relationship. lationships and their properties are captured in order to model An object is defined as an actor or a component of a system an IoT system architecture. TORTE maps each relationship under development (SUD). The UML 2.5 specification [5] TABLE I T HE TYPES OF ARCHITECTURAL OBJECTS Type Description user Users using or maintaining other objects. service Services provided for other objects and deployed in cyberspace. edge Edges constructing networks and deployed in physical space. device Devices controlling or monitoring other objects and deployed in physical space. energy Energy suppliers transmitting energy for other objects and deployed in physical space. environment Natural environment stimulating other objects or monitored them. TABLE II T HE TYPES OF ARCHITECTURAL RELATIONSHIPS Type Description use An object uses a beneficial service of another object. request An object requires data from another object. control An object changes or maintains behaviors of another actor. monitor An object monitors another object without requiring a response. transmit-data An object transmits data to another object. transmit-energy An object transmits energy to another object. (a) (b) Fig. 1. A model example and the tool defines an actor as follows: “an actor specifies a role played existing layers. by a user or any other system that interacts with the subject.” III. M ODEL V ERIFICATION That is, actors interact with a SUD from the outside and their capability cannot be changed by the developers of the SUD. Fig 2 shows the overview of the model verification process. This research assumes that architectural elements, i.e. objects Meanwhile, components behave as a part of a SUD and and relationships, have common behaviors for each type of their capability can be changed by the developers of the SUD. element. For instance, the behaviors include interaction proto- When use cases and their relationships are given to models, the cols when controlling, monitoring or transmitting something. models have the aspect of a use case diagram [5]. Hence, the The combinations of such behaviors across different objects models have an architectural view in the twin peaks model [2], should be verified at an early stage of the design phase. Hence, [1] when use case models are assumed to be a requirements our method employs the logic programming language Prolog view. for the verification. According to existing research [7], [8], [9] on IoT system According to the ISO/IEC standard of Prolog [10], A development, relationships have been variously categorized but program in Prolog consists of many clauses. Each clause is are different from each other. Thus, an architectural design categorized into either a fact or a rule. Fact clauses can model should have the flexibility to easily accept new view- be completely generated from model elements in TORTE. points, i.e. relationship types. TORTE can easily accept new Table III shows the correspondences between model ele- viewpoints by adding corresponding layers without affecting ments and the resulting fact clauses. Bracketed strings, e.g. Architectural model Generate fact clauses in Prolog and execute the resulting program Input Output Tool to edit and Rule clauses in Prolog verify the model Result highlighted on layers Fig. 2. Overview of the model verification process TABLE III C ORRESPONDENCES BETWEEN MODEL ELEMENTS AND fact CLAUSES Model elements Fact clauses Each object object([name], [type]). Each relationship r([type], [source], [target]). Each object property [property’s name]([object’s type], [object’s name]). [name], represent variables which are replaced with model to create relationships including their respective types; (2) six elements or their properties in the generation. For instance, class diagrams representing their respective layers can be auto- a camera object categorized as device is transformed into matically generated in order to intuitively confirm the result of object(camera, device). inputs; (3) a round trip-engineering function is implemented Meanwhile, rule clauses pre-defined by TORTE represent in order to guarantee the consistency between inputs to the common behaviors using model elements and their properties. editor and the corresponding class diagrams. For instance, an Listing 1 shows the rule clauses excerpted. For instance, the association and its stereotype represent a relationship and its clause notEnergySupplied(X, Ls) aims to discover whether type, which correspond to a cell in a matrix-based input form. there is a path in which an edge, device or energy supplier When such an association is removed, the corresponding cell cannot receive energy from any power source. When such is unchecked automatically. a path existed, the objects and relationships in the path are The verifier part of the tool provides the following features: highlighted with red on the transmit-energy layer. In (1) fact clauses in Prolog can be automatically generated this demonstration, we assume that only these types of objects from a model in TORTE in order to verify the model; (2) cannot work without the energy generated in the system. The an input form is provided in order to give a query to the clause checkDataTransmission(X) aims to discover the edges program; (3) the program is executed by using JIProlog [12], and devices that cannot transmit any data because of lack a Prolog implementation in Java, as a checker component; (4) of energy. This clause is defined by slightly extending the the execution result can be highlighted on the model in order clause notEnergySupplied(X, Ls). Thus, various clauses can to give feedback to the developer. be easily created by reusing existing clauses in accordance with the relationship between layers in order to easily and V. P RELIMINARY E VALUATION variously verify the model. Currently, if users want to extend As a preliminary evaluation, we applied TORTE to an rule clauses, knowledge of Prolog is necessary. Therefore, in architectural model of an existing farm monitoring system future work we plan to establish a method to create a number [13], [14]. As a result, we confirmed that the tool can output of beneficial rule clauses in line with an architectural model. expected results in some cases. Fig 3 shows an example of A complete program can be generated by combining the the model highlighted. A problem with this model is that rule and fact clauses mentioned above. The rule clauses are the charge controller is not connected to the two DC-DC used for checking whether a certain object can be reached converters on the transmit-data layer. Elements colored from another object along the relationships between them on in red in Fig 3 show the edges, devices and energy suppliers the basis of their behaviors. whose energy cannot be supplied from any power sources, and the edges and devices that cannot transmit any data because IV. A T OOL TO E DIT AND V ERIFY M ODELS of lack of energy. Fig 1(b) shows a tool to edit and verify models created in TORTE. The tool is implemented in Java and as a software VI. C ONCLUSION plug-in for the UML modeling editor Astah* [11]. Astah* pro- This paper presented TORTE, a method of modeling an vides a basic editor for UML diagrams, but adding stereotypes IoT system architecture on the abstraction level of a use case to each element is laborious and error-prone work. model, and verifying the model with a logic programming The editor part of the tool provides the following features: language. A support tool provides an editor part by extending (1) matrix-based input forms to the set of architectural objects an existing UML editor for constructing architectural models, and to each layer are provided in order to edit object types and which describe various relationships and relevant objects in 1 /** 2 * notEnergySupplied(X, Ls): clauses to identify 3 * the paths Ls that energy cannot be transmitted. 4 * The paths must include the object X. 5 */ 6 notEnergySupplied(X, Ls) :- 7 (object(X, device); 8 object(X, edge); 9 object(X, energy)), 10 notEnergySupplied(X, Ls, []). 11 12 notEnergySupplied(X, Ls, Lp) :- 13 not(source(energy, X)), 14 not(r(transmit_energy, _, X)), 15 Ls = [X|Lp]. 16 17 notEnergySupplied(X, Ls, Lp) :- 18 not(source(energy, X)), 19 r(transmit_energy, Y, X), 20 member(Y, Lp), 21 Ls = [Y, X|Lp]. 22 23 notEnergySupplied(X, Ls, Lp) :- 24 not(source(energy, X)), 25 r(transmit_energy, Y, X), 26 not(member(Y, Lp)), 27 notEnergySupplied(Y, Ls, [X|Lp]). 28 /** 29 * checkDataTransmission(X): clauses to identify 30 * whether the object X can work by obtaining energy. 31 */ 32 checkDataTransmission(X) :- 33 (object(X, device); 34 object(X, edge)), 35 notEnergySupplied(X). 36 37 notEnergySupplied(X):- 38 notEnergySupplied(X, Ls). Listing 1. Rule clauses in Prolog (excerpt) Transmit-data Transmit-energy Fig. 3. Highlight of an execution result IoT systems. The tool also provides a verifier part by using Prolog. As future work, we plan to add beneficial rules to check on the basis of the failure histories of IoT systems. We subsequently evaluate TORTE by applying it to various large- scale systems. ACKNOWLEDGMENT This work was supported by JSPS KAKENHI Grant Num- ber JP15K00097 and JP17KT0043, and the Telecommunica- tions Advancement Foundation. R EFERENCES [1] B. Nuseibeh, “Weaving together requirements and architectures,” Com- puter, vol. 34, no. 3, pp. 115–117, 2001. [2] J. Cleland-Huang, R. S. Hanmer, S. Supakkul, and M. Mirakhorli, “The twin peaks of requirements and architecture,” IEEE Software, vol. 30, no. 2, pp. 24–29, 2013. [3] E. Yu, P. Giorgini, N. Maiden, J. Mylopoulos, and S. Fickas, Modeling Strategic Relationships for Process Reengineering. MIT Press, 2011, pp. 11–152. [4] A. van Lamsweerde and L. Willemet, “Inferring declarative require- ments specifications from operational scenarios,” IEEE Transactions on Software Engineering, vol. 24, no. 12, pp. 1089–1114, 1998. [5] Object Management Group. (2015) Unified model- ing language. (Accessed: 2016-10-04). [Online]. Available: http://www.omg.org/spec/UML/2.5/ [6] E. S. K. Yu, “Towards modeling and reasoning support for early-phase requirements engineering,” in Proceedings of the 3rd IEEE International Symposium on Requirements Engineering, ser. RE ’97, 1997, pp. 226– 235. [7] (2015) Industrial internet reference architecture version 1.7. (Accessed: 2016-07-27). [Online]. Available: http://www.iiconsortium.org/IIRA-1- 7-ajs.pdf [8] L. Atzori, A. Iera, and G. Morabito, “The internet of things: A survey,” Computer Networks, vol. 54, no. 15, pp. 2787–2805, 2010. [9] P. Patel, B. Morin, and S. Chaudhary, “A model-driven development framework for developing sense-compute-control applications,” in Pro- ceedings of the 1st International Workshop on Modern Software Engi- neering Methods for Industrial Automation, 2014, pp. 52–61. [10] “Information technology – Programming languages – Prolog – Part 1: General core,” International Organization for Standardization, Standard, 1995. [11] Change Vision, Inc. astah professional. [Online]. Available: http://astah.net/ [12] U. Chirico. JIProlog. (Accessed: 2016-11-18). [Online]. Available: http://www.jiprolog.com/ [13] K. Kobayashi and Y. Saito, “Development of hand framing camera for field monitoring,” in Proc. of EFITA-WCCA-CIGR Conference, 2013. [14] K. Kobayashi, Y. Fujikawa, and Y. Saito, “Monorail-based monitoring system for multipoint field observation,” in Proceedings of the 2014 International Workshop on Web Intelligence and Smart Sensing, 2014, pp. 8:1–8:2.