Process algebra is one of the best suitable formal methods to model IoT systems, supporting formal specification and analysis. However when IoT systems are under certain uncertainty, it is necessary to model their unpredictability based on the uncertainty. In other words, process algebra should provide specific features to model predictable behaviors to cover this kind of uncertainty, based on probability concept. There have been several process algebras with probability, such as, PAROMA, PACSR, etc. However they are not well suitable for the smart IoT with complex uncertainty, since they are simply based only on discrete model or exponential model. Consequently, they allows only simple or targeted probability to be specified and analyzed, and they only reveal simple or targeted behaviors of the IoT systems. In order to handle such limitations, the paper presents a new formal method, called dTP-Calculus, extended from the existing dT-Calculus with the discrete, normal, exponential, and the uniform probability models. It provides all the possible probability features for the smart IoT system with complex uncertainty. The specification of the modeling will be simulated statistically for the IoT systems, and further the simulation results will be analyzed for probabilistic properties of the systems. In order to demonstrate practicality of the approach, a tool set for the calculus has been implemented in the SAVE tool set, developed on the ADOxx Meta-Modeling Platform, including Specifier, Analyzer and Verifier. It can be considered as one of the most innovative methods with the practical tools.
Internet of Things (IoT) is one of the most important requirements for Industry 4.0. Especially, Industrial Internet of Things (IIoT) requires correctness and safety of system operations performed by people, in order to guarantee expected industrial production output, as well as to provide safety protection to the people [1]. In addition, it is necessary to provide the capability to predict a variety of system behaviors for the safety protection, detectable from probabilistic system analysis. In order to verify formally such safety requirements of the systems with respect to the characteristics of IoT or IIoT, it is desirable to apply formal methods to the IoT or IIoT systems for formal specification and analysis.
Formal methods are used to verify various properties of the IoT systems, for example, communication protocols and security of the systems [2, 3, 4]. However there is lack of research to verify behavior of the systems in terms of movements of the IoT devices. In order to guarantee safety of the systems, verification of the behavior, as well as of security, is strongly required [5]. Therefore process algebra can be used to verify the IoT systems with the properties of distributedness, mobility and real-time. Generally, it is very difficult to predict various system behaviors with process algebra because of its nondeterministic choice operations. In order to overcome the limitation, a new type of process algebras, such as, PAROMA [6] and PACSR [7], were defined based on the notion of probability. However these process algebras have limitations to specify and analyze very complex systems like IoT or IIoT, since PACSR is capable of specifying probabilistic choice operations in only one form of probability model, that is, discrete model and PAROMA is only based on exponential distribution model. In the IoT systems, various behaviors cannot be predicted from the explicitly fixed or exponentially distributed only probabilistic branch of choice operations, since the systems behave differently according to different specification and requirements. Therefore it is necessary to apply various probabilistic models based on normal, exponential, or other distributions in order to predict various behaviors, instead of being on the fixed or exponential models.
In order to handle this kind of limitations, this paper proposes dTP-Calculus, a probabilistic process algebra extended from dT-Calculus [8] with a set of probability models, in order to specify and analyze probabilistic behaviors of the IoT systems. Note that dT-Calculus was originally designed by the authors to specify a variety of timed movements of processes on virtual geographical space.
Practically, in order to demonstrate the feasibility and applicability of the calculus to the IoT systems, a set of tools, known as SAVE, have been developed on the ADOxx Meta-Modeling Platform. SAVE consists of Specifier, Analyzer and Verifier. And an example, known as Smart Emergency Evacuation System (SEES), has been applied to SAVE for specification and analysis in the calculus. It can be considered one of the most practical tools applied to the IoT system for Industry 4.0.
The paper is organized as follows. The basic definition of dTP-Calculus is described in Section 2. The probabilistic models in the calculus are defined and analyzed with the example in Section 3, and the SAVE tool set [9] to model the calculus is described in Section 4. Finally conclusions and future research will be discussed in Section 5. dTP-Calculus
dTP-Calculus is a process algebra extended from existing dT-Calculus in order to define probabilistic behavioral property of processes on the choice operations. 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 virtual geographical space. The syntax of dTP-calculus is shown in Fig. 1. 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 ter minated at the same time. 2.2
There are 4 types of probabilistic models to specify probabilistic choice as follows. Each model may require variables to be used to define probability: 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 and the standard deviation of , whose density function is defined by √12 exp (− ( 2− 2)2). 3) Exponential distribution: This is a probabilistic model based on the exponential distribution with frequency of , whose density function is defined by λe− . 4) tion is defined by { 1
− Uniform distribution: This is a probabilistic model based on the uniform distribution with the lower bound and the upper bound , whose density func0 ( ≤ ≤ ).
Once a model is defined, the conditions for the selection of the branches should be
specified. There are differences in the specifications for the conditions in the models.
In the discrete distribution, the values of the probabilities are specified directly in the
condition as shown in Expression (
{0.7}+ {0.3}
(
( > 52)+ (
3.1
This section demonstrates the applicability of dTP-Calculus to the IoT systems with an example, known as Smart Emergency Evacuation System (SEES). Fig 2 shows the specification of the SEES example in dTP-Calculus. The processes in the example as follows: 1) Control System: The main process to control other processes in case of fire. 2) Sensor: The process to sense 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 Floor and 2nd Floor. And two persons, P1 and P2, in 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 mission in order as follows: 1) A fire occurs on 1st Floor or the 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.
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.
Expressions (
(̅̅̅̅̅̅){0.5}+
(̅̅̅̅̅̅){0.5}
∅ … { < 2.5}+ (
It is possible to analyze the probability of each occurrence of behaviors, that is, escaping or rescuing, by extracting the system behaviors from the SEES example. Even though it is possible to calculate the probability of each occurrence mathematically, in dTP-Calculus, the probability is obtained and analyzed by simulating a significant amount of trials for each occurrences based on the specifications. From the specification, it is possible to analyze all the possible execution paths from the example, as Fig. 3 shows. There are total 8 possible paths, and no system fault, including deadlock, does occur in each cases.
Each path implies each possible system behavior, as shown in Table 1, based on the
following meanings:
1) Fire: The location where the fire occurred.
2) In: P1 and P2, confined in Building.
3) Out: P1 and P2, escaped from Building.
Now it is possible to perform probabilistic analysis mathematically for each path. The
probability in Building is specified directly in the condition of its probabilistic choice,
but the probabilities in P1 and P2 are to be calculated from their distributions.
According to the normal distribution density function, Expression (
∅ … {0.2023}+
∅ … {0.3773}+
2
2
… {0.7977}
… {0.6227}
(
The representative process algebras to specify probability properties of systems can be PAROMA [6] and PACSR [7]. These process algebras allow specifying various probability properties, but they have some limitations to the properties required by the IoT systems. PAROMA allows specifying exponential distribution probability model by using the λ parameter, at the time of defining location information of each agent. Further it is suitable to analyze systems consisting of geographically distributed agents by applying M2MAM (Multi-class, Multi-message Markovian Agent Models) [12]. However, the location information is simply a parameter used for communication, but mobility of the location cannot be expressed properly. PACSR is the process algebra to express resources and probability. It allows specifying three properties of resources, time and probability, as well as exceptional handling using time property, but only simple form of probability using discrete distribution is allowed. However dTP-Calculus allows specifying various properties of geographical space, time and probabilities, suitable to the IoT environments. Geographical mobility, not just simple geographical information, can be expressed, and various types of time properties can be specified, too. More importantly, various probability properties can be specified with 4 kinds of probability models, and change of probability from change of the IoT environment can be more easily specified with probability density function, not with specific predefined probability. In addition, complex probability computation and simulation are automatically performed using the SAVE tool. The analysis of the IoT systems through the simulation increases prediction of nondeterministic behavior of the systems by showing whether the systems operate properly according to the specified probability or not. 6
This paper presented a probabilistic process algebra, known as dTP-Calculus, extended from dT-Calculus. It showed that the calculus allows 4 different types of probabilistic models in order to specify and analyze the IoT systems. It demonstrated that the calculus is capable of specifying and analyzing very complex probabilistic system behaviors, like IoT, based on the probabilistic models.
The paper, also, showed that a suite of tools, known as SAVE, has been developed on ADOxx in order to apply the calculus to real industrial examples in Industry 4.0. It also showed that SAVE can be used for real industrial examples based on different probabilistic cases in order to generate trial-based simulation output, not from the mathematical calculation. dTP-Calculus and SAVE can be considered as one of most innovative modeling methods and tools to specify and analyze very complex system behavior, like IoT, based on probability. The future research will be development of requirements analysis and verification methods for probabilities, and be application of dTP-Calculus and SAVE to real the IoT examples 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(2010-0023787), and Space Core Technology Development Program through the NRF(National Research Foundation of Korea) funded by the Ministry of Science, ICT and Future Planning(NRF2014M1A3A3A02034792), and Basic Science Research Program through the National Research Foundation of Korea(NRF) funded by the Ministry of Education(NRF2015R1D1A3A01019282).