RESUMO
Process algebra is one of the most suitable formal methods to model smart IoT systems for smart cities. Each IoT in the systems can be modeled as a process in algebra. In addition, the nondeterministic behavior of the systems can be predicted by defining probabilities on the choice operations in some algebra, such as PALOMA and PACSR. However, there are no practical mechanisms in algebra either to measure or control uncertainty caused by the nondeterministic behavior in terms of satisfiability of the system requirements. In our previous research, to overcome the limitation, a new process algebra called dTP-Calculus was presented to verify probabilistically the safety and security requirements of smart IoT systems: the nondeterministic behavior of the systems was defined and controlled by the static and dynamic probabilities. However, the approach required a strong assumption to handle the unsatisfied probabilistic requirements: enforcing an optimally arbitrary level of high-performance probability from the continuous range of the probability domain. In the paper, the assumption from the previous research is eliminated by defining the levels of probability from the discrete domain based on the notion of Permissible Process and System Equivalences so that satisfiability is incrementally enforced by both Permissible Process Enhancement in the process level and Permissible System Enhancement in the system level. In this way, the unsatisfied probabilistic requirements can be incrementally enforced with better-performing probabilities in the discrete steps until the final decision for satisfiability can be made. The SAVE tool suite has been developed on the ADOxx meta-modeling platform to demonstrate the effectiveness of the approach with a smart EMS (emergency medical service) system example, which is one of the most practical examples for smart cities. SAVE showed that the approach is very applicable to specify, analyze, verify, and especially, predict and control uncertainty or risks caused by the nondeterministic behavior of smart IoT systems. The approach based on dTP-Calculus and SAVE may be considered one of the most suitable formal methods and tools to model smart IoT systems for smart cities.
RESUMO
Process algebra can be considered one of the most practical formal methods for modeling Smart IoT Systems in Digital Twin, since each IoT device in the systems can be considered as a process. Further, some of the algebras are applied to predict the behavior of the systems. For example, PALOMA (Process Algebra for Located Markovian Agents) and PACSR (Probabilistic Algebra of Communicating Shared Resources) process algebras are designed to predict the behavior of IoT Systems with probability on choice operations. However, there is a lack of analytical methods in the algebras to predict the nondeterministic behavior of the systems. Further, there is no control mechanism to handle undesirable nondeterministic behavior of the systems. In order to overcome these limitations, this paper proposes a new process algebra, called dTP-Calculus, which can be used (1) to specify the nondeterministic behavior of the systems with static probability, (2) verify the safety and security requirements of the nondeterministic behavior with probability requirements, and (3) control undesirable nondeterministic behavior with dynamic probability. To demonstrate the feasibility and practicality of the approach, the SAVE (Specification, Analysis, Verification, Evaluation) tool has been developed on the ADOxx Meta-Modeling Platform and applied to a SEMS (Smart Emergency Medical Service) example. In addition, a miniature digital twin system for the SEMS example was constructed and applied to the SAVE tool as a proof of concept for Digital Twin. It shows that the approach with dTP-Calculus on the tool can be very efficient and effective for Smart IoT Systems in Digital Twin.
RESUMO
This paper presents a new modeling method to abstract the collective behavior of Smart IoT Systems in CPS, based on process algebra and a lattice structure. In general, process algebra is known to be one of the best formal methods to model IoTs, since each IoT can be represented as a process; a lattice can also be considered one of the best mathematical structures to abstract the collective behavior of IoTs since it has the hierarchical structure to represent multi-dimensional aspects of the interactions of IoTs. The dual approach using two mathematical structures is very challenging since the process algebra have to provide an expressive power to describe the smart behavior of IoTs, and the lattice has to provide an operational capability to handle the state-explosion problem generated from the interactions of IoTs. For these purposes, this paper presents a process algebra, called dTP-Calculus, which represents the smart behavior of IoTs with non-deterministic choice operation based on probability, and a lattice, called n:2-Lattice, which has special join and meet operations to handle the state explosion problem. The main advantage of the method is that the lattice can represent all the possible behavior of the IoT systems, and the patterns of behavior can be elaborated by finding the traces of the behavior in the lattice. Another main advantage is that the new notion of equivalences can be defined within n:2-Lattice, which can be used to solve the classical problem of exponential and non-deterministic complexity in the equivalences of Norm Chomsky and Robin Milner by abstracting them into polynomial and static complexity in the lattice. In order to prove the concept of the method, two tools are developed based on the ADOxx Meta-Modeling Platform: SAVE for the dTP-Calculus and PRISM for the n:2-Lattice. The method and tools can be considered one of the most challenging research topics in the area of modeling to represent the collective behavior of Smart IoT Systems.
