Process model to predict nondeterministic behavior of IoT systems

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.