=Paper=
{{Paper
|id=Vol-2019/demos_3
|storemode=property
|title=A Tool to Edit and Verify IoT System Architecture Model
|pdfUrl=https://ceur-ws.org/Vol-2019/demos_3.pdf
|volume=Vol-2019
|authors=Shinpei Ogata,Hiroyuki Nakagawa,Yoshitaka Aoki,Kazuki Kobayashi,Yuko Fukushima
|dblpUrl=https://dblp.org/rec/conf/models/OgataNAKF17
}}
==A Tool to Edit and Verify IoT System Architecture Model==
https://ceur-ws.org/Vol-2019/demos_3.pdf
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.