# Process Algebra to Control Nondeterministic Behavior of Enterprise Smart IoT Systems with Probability

Junsup Song, Moonkun Lee

► To cite this version:

Junsup Song, Moonkun Lee. Process Algebra to Control Nondeterministic Behavior of Enterprise Smart IoT Systems with Probability. 12th IFIP Working Conference on The Practice of Enterprise Modeling (PoEM), Nov 2019, Luxembourg, Luxembourg. pp.184-196, 10.1007/978-3-030-35151-9_12. hal-03231349

HAL Id: hal-03231349

https://inria.hal.science/hal-03231349

Submitted on 20 May 2021

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Process Algebra to Control Nondeterministic Behavior of Enterprise Smart IoT Systems with Probability

Yeongbok Choe, Junsup Song and Moonkun Lee

Chonbuk National University
567 Baekje-daero Deokjin-gu
Jeonju-si Jeonbuk 54896, Republic of Korea
moonkun@jbnu.ac.kr

**Abstract.** Process algebra is one of the best suitable formal methods to model enterprise Smart IoT Systems with some uncertainty of risks. However, because of choice operations in process algebra, it is necessary to control nondeterministic behaviors of the systems. The process algebra, i.e., PAROMA, PACSR, tried to control the degree of selection in the choice operations with probability, but they didn't have any notion of controlling nondeterminism in the systems, since they were based on static probability models only. In order to overcome the limitation, the paper presents a new formal method, called dTP-Calculus, extended from the existing dT-Calculus with dynamic properties on probability. Consequently, it will provide all the necessary probable features to determine the safe and secure range of the system behaviors. For implementation, the SAVE tool suite has been developed on the ADOxx Meta-Modeling Platform, including Specifier, Analyzer and Verifier.

**Keywords:** dTP-Calculus, Formal Method, Probability, Fault-Tolerance, Smart IoT Systems, SAVE, ADOxx Meta-Modeling Platform.

## 1 Introduction

Enterprise Smart IoT Systems, like Smart City, are mostly based on IoT, and are run by Big Data and AI [1, 2, 3]. Because of the complexity and intelligence of the systems, the systems must be provided with some means of controlling the uncertainty caused by the complexity and against the intelligence to handle some probable risks.

In general, it is well known that process algebra is most suitable to model enterprise IoT systems, since each IoT can be considered as a process, and its activities and properties can be represented by those of the process in the algebra [4]. For example, distributedness, mobility, interactivity, control, periodicity, real-time, etc. Further, the unpredictable behavior of the systems from uncertainty can be represented by the unconditional nondeterministic choice operations in the algebra [5], which needs to be controlled by some means. The first method to control nondeterminism was the probability in PAROMA [6] and PACSR [7], based on the static probability models. However the method did not provide some feature to control uncertainty to satisfy thresh-
old to manage risks, caused by nondeterminism, since PACSR was only based on discrete model and PAROMA only on exponential distribution model.

In order to overcome limitations, this paper presents dTP-Calculus [8, 9], a probabilistic process algebra extended from dT-Calculus [10] with dynamic probability properties. The model can control nondeterministic behavior of the system with the dynamic properties determined by the various functional entities. Further the model can be used to manage risks and capability. In order to prove the feasibility of the approach, the paper presents the SAVE tool suite [11] to specify, analyze and verify such systems with dTP-Calculus, developed on ADOxx Meta-Modeling Platform [12].

The paper consists of the following sections. In Section 2, dTP-Calculus is described. In Section 3, the controlling methods for nondeterminism are presented with usage. In Section 4, a Smart City example is specified and analyzed using dTP-Calculus. In Section 5, the SAVE tool is described. In Section 6, conclusions and future research are made.

# 2 dTP-Calculus

## 2.1 Syntax and Semantics

dTP-Calculus is a process algebra extended from existing dT-Calculus in order to define probabilistic behavior of processes on the choice operation. Note that dT-Calculus is the process algebra originally designed by the authors of the paper in order to specify and analyze various timed movements of processes on the virtual geographical space. The syntax of dTP-calculus is shown in Fig. 1.

<figure><img src="image_2.png" /><figcaption>Fig. 1. Syntax of dTP-Calculus</figcaption></figure>

Each part of the syntax is defined as follows:

1) *Action*: Actions performed by a process.

2) *Timed action*: The execution of an action with temporal restrictions. The temporal properties of `[r, to, e, d]` represent ready time, timeout, execution time, and deadline, respectively. *p* and *n* are properties for periodic action or pro-
cesses: *p* for period and *n* for the number of repetition.

3) *Timed process*: Process with temporal properties.

4) *Priority*: The priority of the process *P* represented by a natural number. The higher number represents the higher priority. Exceptionally, 0 represents the highest priority.

5) *Nesting*: *P* contains *Q*. The internal process is controlled by its external process. If the internal process has a higher priority than that of its external, it can move out of its external without the permission of the external.

6) *Channel*: A channel *r* of *P* to communicate with other processes.

7) *Choice*: Only one of *P* and *Q* will be selected nondeterministically for execution.

8) *Probabilistic choice*: Only one of *P* and *Q* will be selected probabilistically. Selection will be made based on a probabilistic model specified with *F*, and the condition for each selection will be defined with *c*.

9) *Parallel*: Both *P* and *Q* are running concurrently.

10) *Exception*: *P* will be executed. But *E* will be executed in case that *P* is out of timeout or deadline.

11) *Sequence*: *P* follows after action *A*.

12) *Empty*: No action.

13) *Send/Receive*: Communication between processes, exchanging a message by a channel *r*.

14) *Movement request*: Requests for movement. *p* and *k* represent priority and key, respectively.

15) *Movement permission*: Permissions for movement.

16) *Create process*: Creation of a new internal process. The new process cannot have a higher priority than its creator.

17) *Kill process*: Termination of other processes. The terminator should have the higher priority than that of the terminatee.

18) *Exit process*: Termination of its own process. All internal processes will be terminated at the same time.

Semantics of all the operations are defined as transition rules as shown in the Table 1.

<table><caption>**Table 1.** Semantics of dTP-Calculus</caption><thead><tr><th>Name</th><th>Transition Rules</th><th>Name</th><th>Transition Rules</th></tr></thead><tbody><tr><td>In</td><td><table><tr><td>P</td><td>in(k) Q</td><td>P in(k)</td><td>P in(k)</td><td>P'</td><td>Q'</td></tr><tr><td>P</td><td>Q</td><td>Q'</td><td>Q'</td><td>P'</td><td>Q'</td></tr><tr><td>P</td><td>Q</td><td>Q'</td><td>Q'</td><td>P'</td><td>Q'</td></tr></table></td><td>Out</td><td><table><tr><td>P</td><td>out(k) Q</td><td>P out(k)</td><td>P out(k)</td><td>P'</td><td>Q'</td></tr><tr><td>P</td><td>Q</td><td>Q'</td><td>Q'</td><td>P'</td><td>Q'</td></tr><tr><td>P</td><td>Q</td><td>Q'</td><td>Q'</td><td>P'</td><td>Q'</td></tr></table></td></tr><tr><td>Get</td><td><table><tr><td>P</td><td>get(k) Q</td><td>P get(k)</td><td>P get(k)</td><td>P'</td><td>Q'</td></tr><tr><td>P</td><td>Q</td><td>Q'</td><td>Q'</td><td>P'</td><td>Q'</td></tr><tr><td>P</td><td>Q</td><td>Q'</td><td>Q'</td><td>P'</td><td>Q'</td></tr></table></td><td>Put</td><td><table><tr><td>P</td><td>put(k) Q</td><td>P put(k)</td><td>P put(k)</td><td>P'</td><td>Q'</td></tr><tr><td>P</td><td>Q</td><td>Q'</td><td>Q'</td><td>P'</td><td>Q'</td></tr><tr><td>P</td><td>Q</td><td>Q'</td><td>Q'</td><td>P'</td><td>Q'</td></tr></table></td></tr><tr><td>InP</td><td><table><tr><td>P<sub>(n)</sub></td><td>in<sup>P</sup>(k) Q<sub>(m)</sub></td><td>P'<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td></tr><tr><td>P<sub>(n)</sub></td><td>Q<sub>(m)</sub></td><td>Q<sub>(m)</sub></td><td>P<sub>(n)</sub></td><td>Q<sub>(m)</sub></td><td>P<sub>(n)</sub></td></tr><tr><td>P<sub>(n)</sub></td><td>Q<sub>(m)</sub></td><td>Q<sub>(m)</sub></td><td>P<sub>(n)</sub></td><td>Q<sub>(m)</sub></td><td>P<sub>(n)</sub></td></tr></table></td><td>OutP</td><td><table><tr><td>P<sub>(n)</sub></td><td>out<sup>P</sup>(k) Q<sub>(m)</sub></td><td>P'<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td></tr><tr><td>P<sub>(n)</sub></td><td>Q<sub>(m)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td></tr><tr><td>P<sub>(n)</sub></td><td>Q<sub>(m)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td></tr></table></td></tr><tr><td>GetP</td><td><table><tr><td>P<sub>(n)</sub></td><td>get<sup>P</sup>(k) Q<sub>(m)</sub></td><td>P'<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td></tr><tr><td>P<sub>(n)</sub></td><td>Q<sub>(m)</sub></td><td>Q<sub>(m)</sub></td><td>P<sub>(n)</sub></td><td>Q<sub>(m)</sub></td><td>P<sub>(n)</sub></td></tr><tr><td>P<sub>(n)</sub></td><td>Q<sub>(m)</sub></td><td>Q<sub>(m)</sub></td><td>P<sub>(n)</sub></td><td>Q<sub>(m)</sub></td><td>P<sub>(n)</sub></td></tr></table></td><td>PutP</td><td><table><tr><td>P<sub>(n)</sub></td><td>put<sup>P</sup>(k) Q<sub>(m)</sub></td><td>P'<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td></tr><tr><td>P<sub>(n)</sub></td><td>Q<sub>(m)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td></tr><tr><td>P<sub>(n)</sub></td><td>Q<sub>(m)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td><td>P<sub>(n)</sub></td></tr></table></td></tr><tr><td>InN</td><td><table><tr><td>P</td><td>in(k) Q</td><td>P in(k)</td><td>P in(k)</td><td>P'</td><td>Q'</td></tr><tr><td>P</td><td>Q</td><td>Q'</td><td>Q'</td><td>P'</td><td>Q'</td></tr><tr><td>P</td><td>Q</td><td>Q'</td><td>Q'</td><td>P'</td><td>Q'</td></tr></table></td><td>GetN</td><td><table><tr><td>P</td><td>get(k) Q</td><td>P get(k)</td><td>P get(k)</td><td>P'</td><td>Q'</td></tr><tr><td>P</td><td>Q</td><td>Q'</td><td>Q'</td><td>P'</td><td>Q'</td></tr><tr><td>P</td><td>Q</td><td>Q'</td><td>Q'</td><td>P'</td><td>Q'</td></tr></table></td></tr></tbody></table>
<table><thead><tr><th>Action</th><th>-<br>A. P &rarr; P<sup>A</sup></th><th>ChoiceL<br>ChoiceR</th><th>P<sub>(n)</sub> &rarr; P'<sub>(n)</sub><br>P<sub>(n)</sub> + Q<sub>(n)</sub> &rarr; P'<sub>(n)</sub></th><th>Q<sub>(n)</sub> &rarr; Q'<sub>(n)</sub><br>P<sub>(n)</sub> + Q<sub>(n)</sub> &rarr; Q'<sub>(n)</sub></th></tr></thead><tbody><tr><td>ChoiceP</td><td>P<sub>(n)</sub> &rarr; P<sub>(n)</sub><br>P<sub>(n)</sub> + Q<sub>(n)</sub> &rarr; P'<sub>(n)</sub></td><td>ParlL<br>ParlR</td><td>P &rarr; P'<br>P &parallel; Q &rarr; P' &parallel; Q<br>P &parallel; Q &rarr; P' &parallel; Q'</td><td>Q &rarr; Q'<br>P &parallel; Q &rarr; P &parallel; Q'</td></tr><tr><td>ParCom</td><td>P &rarr; P', Q &rarr; Q'<br>P &parallel; Q &rarr; P' &parallel; Q'</td><td>NestO<br>NestI</td><td>P &rarr; P'<br>P[Q] &rarr; P'[Q]<br>P[Q] &rarr; P[Q']</td><td>Q &rarr; Q'<br>P[Q] &rarr; P[Q']</td></tr><tr><td>NestCom</td><td>P &rarr; P', Q &rarr; Q'<br>P[Q] &rarr; P'[Q']</td><td>Tick-Time<br>R</td><td>-<br>A<sub>[r, to, e, d]</sub> &rarr; A<sub>[r-1, to, e, d-1]</sub><br>(r &ge; 1)</td><td></td></tr><tr><td>Tick-Time<br>TO</td><td>A<sub>[0, to, e, d]</sub> &rarr; A<sub>[0, to-1, e, d-1]</sub> (to &ge; 1)</td><td>Tick-Time<br>End</td><td>A<sub>[0, to, 0, d]</sub> &rarr; A'<sub>[0, to, 0, d]</sub></td><td>A<sub>[0, to, 0, d]</sub> &rarr; A'</td></tr><tr><td>Tick-Time<br>SyncE</td><td>A|A' &rarr; A''|A'''<br>A<sub>[0, to, e, d]</sub>|A'<sub>[0, to, e, d]</sub>|&&& A<sub>[0, to, e, d]</sub>|A'<sub>[0, to, e, d]</sub>|</td><td></td><td>(r&nu;&delta;) &rarr; A''|A'''<br>(e<sub>1</sub> &ge; 1 &and; e<sub>2</sub> &ge; 1)</td><td></td></tr><tr><td>Tick-Time<br>AsyncE</td><td>A<sub>[0, to, e, d]</sub> &rarr; A<sub>[0, to, e-1, d-1]</sub></td><td>Tick-Time<br>P</td><td>P<sub>[r, to, e, d]</sub> &rarr; P<sub>[r, to, e, d-1]</sub></td><td></td></tr><tr><td>Timeout</td><td>A<sub>[0, 0, e, d]</sub> \ P &rarr; P</td><td>Dead-<br>line</td><td>A<sub>[r, to, e, 0]</sub> \ P &rarr; P</td><td></td></tr><tr><td>Period</td><td>A<sup>p,n</sup><sub>[r, to, e, d]</sub> &rarr; A<sup>p,n-1</sup><sub>[r, to, e, d]</sub> (n &gt; 1)</td><td>Period<br>End</td><td>A<sup>p,1</sup><sub>[r, to, e, d]</sub> &rarr; A'<sub>[r, to, e, d]</sub></td><td></td></tr><tr><td>Probability<br>Choice</td><td>a. P &rarr; P<br>(&Sigma;<sub>i&isin;I</sub> a<sub>i</sub>{p<sub>i</sub>}). P a<sub>i</sub>{p<sub>i</sub>} &rarr; P'</td><td></td><td>(&Sigma;<sub>i&isin;I</sub> a<sub>i</sub> = 1, i &isin; I)</td><td></td></tr></tbody></table>

## 2.2 Probability

There are 4 types of probabilistic models to specify probabilistic choice as follows. Each model may require variables to be used to define probability properties:

1) Discrete distribution: It is a probabilistic model without variable. It simply defines specific value of probability for each branch of the choice operation. There are some restrictions. For example, the summation of the probability branches cannot be over 100%.

2) Normal distribution: It is a probabilistic model based on the normal distribution with the mean value of $\mu$ and the standard deviation of $\sigma$, whose density function is defined by $f(x | \mu, \sigma^2) = \frac{1}{\sigma\sqrt{2\pi}}\exp(-\frac{(x-\mu)^2}{2\sigma^2})$.

3) Exponential distribution: This is a probabilistic model based on the exponential distribution with frequency of $\lambda$, whose density function is defined by $f(x; \lambda) = \lambda e^{-\lambda x} (x \ge 0)$.

4) Uniform distribution: This is a probabilistic model based on the uniform distribution with the lower bound $l$ and the upper bound $u$, whose density function is defined by $f(x) = \begin{cases} 0 & (x < a \lor x > b) \\ \frac{1}{u-l} & (l \le x \le u) \end{cases}$.

## 2.3 Example

As an example, the PBC example is defined in dTP-Calculus as shown Fig. 2. It con-
sists of 3 processes: *P* (for Producer), *B* (for Buffer), and *C* (for Consumer). Note that there are two processes, *R1* and *R2* (for Resource), in *P*. The operational requirements with probability are as follows:

1) *Producer* produces two resources, *R1* and *R2*.

2) *Producer* stores the resources in *Buffer* in order.

3) *Producer* informs *Buffer* of the order of *R1* and *R2*, or *R2* and *R1*.

① The probability of choosing the order of *R1* and *R2* for *Producer* is 0.6; that of *R2* and *R1* is 0.4.

② The probability of choosing the order of *R1* and *R2* for *Consumer* is 0.7; that of *R2* and *R1* is 0.3.

4) *Consumer* consumes the resources from *Buffer* in order.

5) *Consumer* informs *Buffer* of the order of *R1* and *R2*, or *R2* and *R1*.

① The probability of choosing the order of *R1* and *R2* for *Consumer* is 0.5; that of *R2* and *R1* is 0.5.

② The probability of choosing the order of *R1* and *R2* for *Buffer* is 0.8; that of *R2* and *R1* is 0.2.

$P[R1 || R2] || B || C;$

$P = (PB(Send R1){0.6}.put R1.put R2+DBPB(Send R2){0.4}.put R2.put R1).exit;$

$B = (PB(Send R1){0.7}.get R1.get R2+DBPB(Send R2){0.3}.get R2.get R2).$

$(CB(Send R1){0.5}.put R1.put R2+DBCB(Send R2){0.5}.put R2.put R1).exit;$

$C = (CB(Send R1){0.8}.get R1.get R2+DBCB(Send R2){0.2}.get R2.get R1).exit;$

$R1 = P put.B get.B put.C get.exit;$

$R2 = P put.B get.B put.C get.exit;$

<caption>**Fig. 2.** Code for PBC Example</caption>

The pictorial system view of the example is shown in Fig. 3, where *P* and *B* are connected with a channel *PB*, and *P* and *B* with a channel *PB*. Note that the synchronous communications between *P* and *B* on *PB* are uncertain due to the unconditional non-deterministic choice operation, but these are controlled by probability on the choice operation, which causes 4 possible combination of the communication with the probability of 0.42, 0.28, 0.18, and 0.12 from the 0.6 vs. 0.4 of *P* by the 0.7 vs. 0.3 of *B*. Both operations are ruled by the definitions of *ParCom* and *ProbabilityChoice* in Table 1. Similarly, those between *B* and *C* on *BC* are 0.40, 0.40, 0.10, and 0.10 from the 0.5 vs. 0.5 of *B* by the 0.8 vs. 0.2 of *C*.

<figure><img src="image_3.png" /><figcaption>**Fig. 3.** System View for PBC Example with Probabilities</figcaption></figure>
# 3 Control Methods and Usage

## 3.1 Probability Function Management

The left side of Fig. 4 shows the reachability graph of the PBC Example. The top node indicates the 4 possible compositions of the synchronous communication between *P* and *B* on PB, with the probabilities of 0.42, 0.28, 0.18, and 0.12 from the 0.6 vs. 0.4 of *P* by the 0.7 vs. 0.3 of *B*, ruled by the definitions of *ParCom* and *ProbabilityChoice* in Table 1. Notice that the middle 2 cases are of deadlock. From the left-most and the right-most compositions show the normal compositions without deadlock, from which another following synchronous communication between *B* and *C* on *BC*, with the probabilities of 0.40, 0.40, 0.10, and 0.10 from the 0.6 vs. 0.4 of *P* by the 0.7 vs. 0.3 of *B*, ruled by the same definitions in Table 1, resulting the compositions of two probabilities to be 0.168, 0.168, 0042, and 0.042 for the right-most, and 0.048, 0.048, 0.012, and 0.012 for the left-most. Notice that the middle 2 cases are of deadlock for both compositions. Finally we can see that the total probability of the safe execution paths without deadlock is 0.27, as shown at the bottom node of the graph. Sometimes the results are not acceptable, and it is necessary to increase the total system probability by changing the probabilities of the nondeterministic choice operations for *P* and *B*, as well as *B* and *C*. For example, as the left side of Fig. 4 shows:

3) *Producer* informs *Buffer* of the order of *R1* and *R2*, or *R2* and *R1*.

① The probability of choosing the order of *R1* and *R2* for *Producer* is 0.9; That of *R2* and *R1* is 0.1.

② The probability of choosing the order of *R1* and *R2* for *Consumer* is 0.79; That of *R2* and *R1* is 0.1.

5) *Consumer* informs *Buffer* of the order of *R1* and *R2*, or *R2* and *R1*.

① The probability of choosing the order of *R1* and *R2* for *Consumer* is 0.9; That of *R2* and *R1* is 0.1.

② The probability of choosing the order of *R1* and *R2* for *Buffer* is 0.9; That of *R2* and *R1* is 0.1.

As a result, the final probability is increased to 0.6724 from 0.27. Further it is possible to define some function with the probability variables in order to control dynamically the acceptable probability for the systems.

<figure><img src="image_4.png" /><figcaption>Fig. 4. Reachability Execution Trees for PBC Example with Probability</figcaption></figure>
## 3.2 Risk Management

In the business applications, there are a number of transactions or decisions to be made in the systems, while managing some risks. Similarly, in the industrial applications, there are a number of interactions to be made by synchronization or nondeterministic selections in the IoT systems, while managing some faults. In either case, it is necessary to evaluate the critical value to tolerate the risks or faults, while performing the specified operations.

The left graph in Fig. 5 shows the case from the PBC example, where a specific execution path is to be selected while performing the operations in order to satisfy the risk or fault tolerance rate less than 0.2, which is the right-most path among all 4 possible paths. More specifically, from the top node, the right-most execution path, that is, the synchronous communication between *P* and *B* on PB for transferring resource *R2* and R1 in order, is selected since the risk or fault-tolerance rate is 0.01, which is less than 0.2 in the requirement. Similarly, from that right-most node, the right-most execution path, that is, the synchronous communication between *B* and *C* on BC for transferring resource *R2* and R1 in order, is selected since the risk or fault-tolerance rate is 0.01, which is less than 0.2 in the requirement. In case that there is no path that satisfies the rate, it will be necessary to change the probabilities dynamically in order to decrease the rate under the acceptable level.

<figure><img src="image_5.png" /><figcaption>Fig. 5. Path Selection for Risk Management and Process Substitution for Capability Management</figcaption></figure>

## 3.3 Capability Management

Sometimes, it is necessary to substitute one IoT with another IoT while managing same capability in the IoT Systems. In order to satisfy the capability requirements for the substitution, there should be some way of evaluating the capability with respect to probability in order to control uncertain for substitution. In the dTP-Calculus, the probability determines the degree of nondeterminism during the choice operations and effects the final system probabilities. For example in the PBC example, the top system view from the right graph in Fig. 5 shows 0.27 of safe system executions without deadlock, where Process *P*<sub>i</sub> has a successful choice operation with the 0.6 probability. Somehow there is a problem that *P*<sub>i</sub> does not work properly and needs to be replaced. Then it is necessary to evaluate which process is suitable for replacement. As the bottom system of the figure shows that, if *P*<sub>j</sub> has a successful choice operation with the 0.7 probability and satisfies the probability based system similarity with the tolerance of less than 0.05, that is, 0.29, it can be replaced for *P*<sub>i</sub>. The process can represent any person, agent, thing, or device in a system.
## 4 A Smart City Example: SEES on SAVE

This section demonstrates the applicability of dTP-Calculus to a Smart City Example based on the IoT systems, known as *Smart Emergency Evacuation System* (SEES), on the SAVE tool, which is developed on the ADOxx Meta-Modeling Platform.

<figure><img src="image_6.png" /><figcaption>**Fig. 6.** dTP-Calculus Code for SEES Example</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>**Fig. 7.** dTP-Calculus Code for SEES Example</figcaption></figure>

### 4.1 Specification

Fig. 6 and 7 show both the dTP-Calculus specification and the system view for the SEES example. The processes in the example as defined as follows:

1) *Control System*: The main process to control other processes in case of fire.

2) *Sensor*: The process to detect fires on Stair A and Stair B.
3) *Building*: The process to represent the building where the fire occurs. It contains all the related processes in the building, except 911.

4) *Floor*: The process to represent the floors in the building. There are two floors: 1st and 2nd Floors. And two persons, P1 and P2, on 2nd Floor.

5) *Stair*: The process to represent stairs. There are two stairs: Stair A and Stair B. A fire occurs at one of the stairs.

6) *Person*: The processes to represent the persons in the building, P1 and P2.

7) 911: The process to perform fire extinction and people rescue.

SEES performs its operations in order as follows. Note that each action is denoted with the number, representing action or interactions from Fig. 6 and 7:

1) A fire occurs on 1st Floor or 2nd Floor: ①.

2) Sensor detects the fire and sends a signal to Control System: ②.

3) *Control System* informs *Person* of the fire and shows the escape route. And it sends the signal to 911: ④.

4) Each *Person* may get out of *Building* safely, or be confined on 2nd Floor: ⑤, ⑥, ⑦, ⑧.

5) *Building* detects the escape of *Person*, and sends the information of the escaped to *Control System*: ⑨.

6) *Control System* sends the information of the confined to 911: ⑩.

7) 911 enters *Building*, extinguishes the fire on 2nd Floor, and rescues *Person* if any: ⑪.

A fire occurs at Stair A or Stair B in Building, and each *Person* may or may not escape from *Building*. In SEES, three kinds of probabilistic choices are specified as follows:

1) *Building*: $SA(Fire)\{0.5\}+_D(SB(Fire)\{0.5\})$

2) P1: $\emptyset$ ... $\{0.2\}+_{D} out \ 2nd \ ... \ \{0.8\}$

3) P2: $\emptyset$ ... $\{0.4\}+_{D} out \ 2nd \ ... \ \{0.6\}$

For simplicity, all the probabilities are defined to be of discrete distribution. For the first probability, it is assumed that the probabilities of detecting a fire from Sensor A and B are same: 0.50 vs 0.50. For the second probability, it is assumed that the probabilities for Person 1 to escape from Building by himself to be 0.80, and that of not escaping 0.20, in which case he is to be rescued by 911. Similarly, for the last probability, that of escaping for Person 2 to be 0.60, and that of not escaping to be 0.40.

## 4.2 Probability Analysis

The left side graph in Fig. 8 is the execution model for SEES, generated by SAVE. Note that there are total 8 paths in the figure, where each path represents the status how Person P1 and P2 are escaped or rescued safely. The right side of the figure
shows the probability of each path, where *P1* or *P2* indicates the status of being es-
caped from Building and *P1'* or *P2'* indicates the status of being rescued by 911.

<figure><img src="image_8.png" /><figcaption>Fig. 8. Execution Model for SEES and its Probabilistic Execution Tree</figcaption></figure>

The top node of the tree shows the probability of detecting a fire from Sensor A and B are same: 0.50 vs 0.50. The second nodes from the first nodes show two probabilities: 1) the probability for Person 1 to escape from Building by himself to be 0.80, and that of not escaping 0.20, as shown in the left box from the nodes, and 2) the probability of Person 2 to be 0.60, and that of not escaping to be 0.40, as shown in the right box from the nodes. The third nodes from the second nodes show two types of all the combinations of the probabilities: 1) the combinations of probabilities for P1 and P2 are 0.48, 0.32, 0.12, and 0.08 from the 0.8 vs. 0.2 of P1 by the 0.6 vs. 0.4 of P2, as shown in the top box from the nodes, and 2) the combinations of its probabilities with the sensor probability are 0.24, 0.16, 0.06, and 0.04 by 0.5 of Sensor A or B, as shown in the bottom box from the nodes. From the tree, it can be analyzed that the probability for both P1 and P2 to escape from the building is 0.48 in total, the probability for either P1 or P2 to do is 0.44 in total, and the probability for both P1 and P2 not to do is 0.08 in total. If the final probabilities are not acceptable, it is possible to change dynamically the probabilities for detecting fires and guiding people to safe evacuation routes by increasing the number of sensors for better visibility and temperature in air.

5 SAVE

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 the following basic three components:

1) Specifier, as shown in Fig. 9, is a tool to specify the IoT systems with dTP- Calculus, visually in the diagrammatic representations [2]. The left side of Fig. 9 is the In-the-Large (ITL) model, or system view, representing both inclusion relations among components of the system and communication channels
among them. The right side of the Fig. 9 is In-the-Small (ITS) models, or pro-
cess view, representing a sequence of the detailed actions, interactions and
movements performed by a process.

2) Analyzer is a tool to generate the execution model from the specification in order to explore all the possible execution paths, as the left side of Fig.10 shows, and to perform the simulation of each execution from the execution model in order to analyze probabilistic behaviors of the specified system.

3) Verifier is a tool to verify a set of system requirements on the geo-temporal space output generated from each, as the right side of Fig. 10 shows. It checks the behaviors of the system for safety and security requirements and shows their results on the output.

<figure><img src="image_9.png" /><figcaption>Fig. 9. Specification Tool of SAVE</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Fig. 10. Analysis and Verification Tool of SAVE</figcaption></figure>

6 Conclusions and Future research

This paper presented dTP-Calculus in order to model enterprise Smart IoT Systems, like Smart City, with uncertainty to safety and security of the systems. It showed that the algebra can be used to control the uncertainty with dynamic probability features on the unconditional nondeterministic choice operations, and that the algebra can provide good facilities to manage risks and capabilities with the systems. Further the paper presented the SAVE tool to demonstrate the feasibility of the approach with the calculus. It can be considered to be one of the innovative methods to handle the uncertainty for enterprise Smart IoT Systems.
The future research will include application of dTP-Calculus and SAVE to real enterprise industry examples to demonstrate their efficiency and effectiveness as method and tool.

## Acknowledgment

This work was supported by Basic Science Research Programs through the National Research Foundation of Korea(NRF) funded by the Ministry of Education(2010-0023787), 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 Education(NRF-2015R1D1A3A01019282), and Hyundai NGV, Korea, and Research Fund from Chonbuk National University (2018~2019).

## References

1. Skouby.K.E., Lynggaard P.: Smart home and smart city solutions enabled by 5G, IoT, AAI and CoT services. In: 2014 International Conference on Contemporary Computing and Informatics (IC3I), pp.874-878, IEEE (2014).

2. Chin, J., Callaghan, V., and Lam, I.: Understanding and personalising smart city services using machine learning, the internet-of-things and big data. In: 2017 IEEE 26th International Symposium on Industrial Electronics (ISIE), pp. 2050-2055, IEEE (2017).

3. Allam, Z., Dhunny, Z. A.: On big data, artificial intelligence and smart cities. Cities, 89, 80-91 (2019).

4. Choe, Y., Lee, M.: Algebraic Method to Model Secure IoT. Domain-Specific Conceptual Modeling, pp.335-355, Springer, (2016).

5. Meldal, S., Walicki, M.: Nondeterministic Operators in Algebraic Frameworks. Computer Systems Laboratory, Stanford University (1995).

6. Feng, C., Hillston, J.: PALOMA: a process algebra for located Markovian agents. In: International Conference on Quantitative Evaluation of Systems, pp.265-280, Springer, Cham (2014).

7. Lee, I., Philippou, A and Sokolsky, O.: Resources in process algebra. The Journal of Logic and Algebraic Programming, 72(1), 98-122 (2007).

8. Choe, Y., Lee, M.: Process Model to Predict Nondeterministic Behavior of IoT Systems. In: Proceedings of the 2nd International Workshop on Practicing Open Enterprise Modeling within OMiLAB (PrOse), (2018).

9. Song, J., Choe, Y., and Lee, M.: Application of Probabilistic Process Model for Smart Factory Systems. In: Knowledge Science Engineering Management (KSEM), (2019).

10. Choe, Y., Lee, S., and Lee, M.: dT-Calculus: A Process Algebra to Model Timed Movements of Processes. International Journal of Computers, 2, 53-62 (2017).

11. Choe, Y., Lee, S., and Lee, M.: SAVE: an environment for visual specification and verification of IoT. In: 2016 IEEE 20th International Enterprise Distributed Object Computing Workshop (EDOCW), pp. 1-8, IEEE (2016).

12. Fill, H. G., Karagiannis, D.: On the Conceptualisation of Modeling Methods Using the ADOxx Meta Modeling Platform. In: Proceedings of Enterprise Modeling and Information Systems Architectures (EMISAJ), 8(1), pp. 4-25, (2013).