Visual representation for operational requirements for Smart IoT Systems is desirable in process algebra, since it is more intuitive than textual representation. Further visual representation for safety requirements in the systems is more desirable in real-time logic since it reduces the complexity of verification of the requirements. However it is not well known that there are common logics for such visualization. In that purpose, this paper presents a visual logic, called GTS Visual Logic, to specify and verify the geo-temporal safety requirements for Smart IoT Systems specified with a process algebra, called dTCalculus. The calculus is used to specify the operational requirements for the systems on some conceptual geographical space. Once they are specified, a set of simulations can be performed to construct all possible execution cases for the requirements, and a set of outputs are produced in terms of processes, their actions and interactions, and dependencies on the 2-dimentional geo-temporal space. Then the visual logic is used to specify and verify all the safety requirements for the systems in terms of dependencies, especially precedencies and conditions, among all the processes, their independent actions and synchronous interactions. For feasibility, a tool, called GTS-VLT, was developed on ADOxx as a basic component of the SAVE tool suite, which is the tool set to model Smart IoT Systems, in order to demonstrate the feasibility of the logic.
One of the main objectives of Industry 4.0 may rely on Smart IoT Systems for
automation with AI and Big Data [
Note that, in general, the requirements for the IoT systems can be classified into two
types of requirements: 1) operation and 2) safety requirements. Mostly the operation
or operational requirements are specified with process algebra, and the safety
requirements are specified with logic, especially, first-order logic [
Note that GTS-VL is a first-order logic to represent all the processes, their
independent actions and synchronous interactions, and, especially, dependencies among
processes, actions and dependencies, visually on the space. It can reduce drastically the
complexity of derivation and reduction steps of verification for the requirements over
their textual representation. Note that the definition of the textual logic has been
reported in [
In order to demonstrate the feasibility and applicability of the logic for the IoT
systems, a tool, called GTS-VLT, has been developed on ADOxx as a basic component
of the SAVE tool suite, which is the tool set to model Smart IoT Systems. Fig. 2
shows the snapshot of the tool for visual verification of two simple safety
requirements for an example. As noted in the figure, one of the main objectives of the
visualization in the tool is WYSWYG: What You See is What You Get. The approach with
the tool can be considered as one of the most innovative visual tools for visual
specification and verification of the safety requirements for the IoT systems.
The paper is organized as follows. The visual definition of GTS-VL is described in
Section 2. The GTS-VLT will be demonstrated with a simple example in Section 3.
The method will be compared with other textual methods in Section 4. The SAVE
tool set [
GTS Visual Logic (GTS-VL) is a first-order logic defined in [
3) Movement permission: Permissions for movement.
Note that timed action is an action with temporal properties of [r, to, e, d], where each represents ready time, timeout, execution time, and deadline, respectively. p and n are properties for periodic action or processes: p for period and n for the number of repetition. When a system is executed in a specific space in time, the system generates all the traces with the actions and interactions of the processes in the systems. These traces can be represented in its GTS as shown in Fig. 4. It consists of two dimensions: one for the geographical, and another for the temporal. There are three difference types of blocks: System Block (S), Process Block (P) and Action Block (A). By definition, a system contains processes, and a process contains actions. Further an interaction is represented as an Interaction Block (I) between two synchronous Action blocks of two different Processes. 2.2
Mostly the safety requirements imply the dependencies among processes, actions, and
interaction block in GTS, with some additional conditions and predicates. Fig. 5
shows some of predicates in GTS Logic with visual representation on GTS. The
temporal and geographical relations among action blocks are visually defined in Fig. 6
and 7. Note that each Ai implies Action Block, and tj does of the temporal properties
for the block defined in the previous section. All the detailed definitions of the spatial
and temporal relations and the predicates are reported in the [
This section demonstrates the applicability of GTS-VL to the IoT systems with a simple example, known as Producer-Buffer-Consumer (PBC). 3.1
There are two types of requirements for the PBC example: 1) Operational Requirements: • Producer produces two resources, R1 and R2. • Producer stores the resources in Buffer in sequence. • Producer informs Buffer of the order of R1 and R2, or R2 and R1. • Consumer consumes the resources from Buffer in order.
• The sequence of the consumption is informed to Buffer by Consumer. 2) Secure Requirements • The sequence should not be violated, since the first resource contains security information to decode the second resource. • The propagation between the first and the second should be less than 30 seconds. • The resources produced by Producer should be consumed by Consumer less than 5 minutes.
2 + (̅̅̅̅̅̅̅̅̅̅2̅). 2 + ( 2). 2. 2. 1). 1). 1. 2.
= [ 1 ∥ 2] ∥ ∥ = ( (̅̅̅̅̅̅̅̅̅̅1̅). = ( ( = 1 = 2 = 1. 1). 2. . . 1. 1. .
. . . . .
Fig. 8 Specification of the PBC Example in the Textual dT-Calculus. 3.2
dT-Calculus for Visualization iii. Once the resources are released off P by P, B gets the resource in B in that sequence of the release, synchronously, with the synchronous passive movement operations between B and R, that is, the get R of B and the B get of R. iv. Once the resources are moved into B by B, B releases the resource off B in the sequence R1 followed by R2, synchronously, with the synchronous passive movement operations between B and R, that is, the put R of B and the B put of R. v. Once the resources are released off B by B, C gets the resource in C in the sequence of the release, synchronously, with the synchronous passive movement operations between C and R :the get R of C and the C get of R. There are two forms of visualization for the example as follows: 1) ITS (In-The-Small) View: It is a process view to visualize the above description in 4). A set of the views for all the processes in the example is shown in Fig. 9. 2) ITL (In-The-Large) View: It is a system view to visualize the above description between 1) and 3). The view for the example is shown in Fig. 10. Note that the views in the figures are the snapshots of the example for visual specification of the example with the tool developed by authors, namely, SAVE/GTS-VLT, on the ADOxx Meta-Modeling Platform. There are two ways of specifying the requirements in dT-Calculus: 1) Textual specification: The specification can be input to SAVE just as shown in
Fig. 8, and ITL and ITS views are automatically generated by SAVE. 2) Visual specification: The requirements can be directly specified in the graphical editor for ITL and ITS views in SAVE.
Once the specification is done, SAVE generates all the possible execution paths of the system. Fig. 11 shows that there are four possible paths in the PBC example: One for the sequence of R1 and R2, another for that of R2and R1, and two deadlock cases. 3.3
Fig. 12 shows the simulation output of the first path for the execution paths of the
example shown from Fig. 11. All the elements of the GTS blocks are shown in the
figure: System, Process and Action Blocks. Further Interactions are shown in the
edges between two synchronous action blocks, as follows:
• τ: Communication
▫ 1 = ( : , (̅̅̅̅̅̅̅̅̅̅1̅), : ( 1))
▫ 2 = ( : , (̅̅̅̅̅̅̅̅̅̅2̅), : ( 2))
• δ: Movements
▫ 1,1 = ( : 1, 1: ) 1,2 = ( : 2, 2: )
▫ 2,1 = ( : 1, 1: ) 2,2 = ( : 2, 2: )
▫ 3,1 = ( : 1, 1: ) 3,2 = ( : 2, 2: )
▫ 4,1 = ( : 1, 1: ) 4,2 = ( : 2, 2: )
The figure also shows a couple of the safety requirements for the PBC example from
Section 3.1. Note that the requirement edges are of the predicates shown in Fig. 5.
The whole requirements are as follows:
• 1 = 1 → ∀ : ( ,1 < ,2) [ = 1,2] : After 1, that is, the communication for
exchange of the resources in the sequence of R1 and R2, all the movements
actions of the resources, that is, , , must follow that sequence.
• 2 = 2 → ∀ : ( ,2 < ,2) [ = 1,2] : Similarly, After 2, that is, the
communication for exchange of the resources in the sequence of R2 and R1, all the
movements actions of the resources, that is, , , must follow that sequence.
• 3 = 1 ∨ 2 < 1,1 ∧ 1,2: After 1 or 2, that is, the sequence of R1 and R2 is
determined between P and B, both resources can be moved from P to B.
• 4 = 1,1 < : ( 1) : Once R1 is moved off P by P, B can get it into B.
• 5 = 1,2 < : ( 2) : Once R2 is moved off P by P, B can get it into B.
• 6 = 2,1 < : ( 1) : Once R1 is moved into B by B, B can put it off B.
• 7 = 2,2 < : ( 2) : Once R2 is moved into B by B, B can put it off B.
• 8 = 3,1 < : ( 1) : Once R1 is moved off B by B, C can get it into C.
• 9 = 3,2 < : ( 2) : Once R2 is moved off B by B, C can get it into C.
• Disadvantages over GTS-VL:
◦ These temporal-based logics have limitations to represent movements.
◦ No visual capability to represent graphically specification and verification of
systems because they are based on text representation.
• Spatial-based logics: Region and Connection calculus (RCC)[
◦ RCC is a spatial logic that distinguishes each space by defining a relationship
between each space.
◦ CRD is a spatial logic based on coordinate system, and it is spatial logic that
distinguishes each space according to coordinates.
• Disadvantages over GTS-VL:
◦ The space of a process can be represented visually, but its mobility is not.
◦ No visual capability to represent temporal properties of processes in
specification and analysis of systems because they are based on textual
representation only.
In order to demonstrate the advantages of the GTS-VL approach, we analyze the
complexity of the analysis and verification process for GTS-VL to its textual
representation. Fig. 13 shows the first requirement from the PBC Example in the GTS-VL
on the GTS output of the simulation for the first execution path of the example, from
Fig. 12. The right side of the figure is the syntax tree of the requirement in the textual
representation, consisting of ’s and ’s, which are also structured in syntax trees of
all the system, process and action blocks with temporal properties. Such trees
generate severe complexity during analysis and verification processes of the requirement in
the form of textual representation. The left side of the figure is the final result that
SAVE/GTS-VLT generates at the end of the analysis and verification process for
GTS-VL over the simulation output on GTS. It drastically simplifies the complexity,
as Table 1 shows. In general, it is well known that the visual method for
communication of information is better than the textual method [
SAVE is a suite of tools to specify and analyze the IoT systems with dTP-Calculus. It
is developed on the ADOxx Meta-Modeling Platform. SAVE consists of basic five
components: Specifier, Execution Model Generator (EMG), Simulation, Analyzer and
Verifier. Specifier is a tool to specify the IoT systems with dT-Calculus, visually in
the diagrammatic representations. EMG is a generator to construct all the possible
execution paths for the system specified in Specifier. Simulation is the main engine to
execute each execution path selected from the execution model in EMG. Analyzer
and Verifier are tools to analyze and verify the safety requirements of the system
specified in GTS-VL. The basic tool of SAVE/GTS-VLT consists of these two
components. All the figures shown in the paper are the snapshots of SAVE/GTS-VLT
generated for the PBC Example. The SAVE tool is an open SW that has been
developed as a project within the Open Models Laboratory (OMiLAB) [
This paper presented a visual method to specify and verify geo-temporal requirements for dT-Calculus, based on GTS-VL. Further SAVE/GTS-VLT was developed to demonstrate the feasibility of the method, based on the ADOxx Meta-Modeling Platform. With the tool, a small example, PBC, was selected for applicability of the method in steps by generating all necessary artefacts for the example: ITL and ITS views, GTS simulation output, GTS-VL requirements. The method with the tool may be considered to be one of the most innovative approaches to specify and verify the operation and safety requirements of Smart IoT Systems. The future research will include development of requirements analysis and verification methods for Smart IoT examples in field for Industry 4.0 in order to show its efficiency and effectiveness.
This work was supported by Basic Science Research Programs through the National Research Foundation of Korea(NRF) funded by the Ministry of Education(20100023787), Space Core Technology Development Program through the National Research Foundation of Korea(NRF) funded by the Ministry of Science, ICT and Future Planning(NRF-2014M1A3A3A02034792), Basic Science Research Program through the National Research Foundation of Korea(NRF) funded by the Ministry of Educa