### Proof of Concepts  
In order to prove the feasibility of the approach in the paper, we developed a visual tool suite called SAVE (Specification, Analysis, Verification, Evaluation), and applied the approach to a smart EMS (emergency medical service) system [11; 12]. Here, the smart EMS system is the system to improve the quality and efficiency of EMS using IoT technology. It not only increases the survival rate of the critical patients but also provides medical personnel with instantaneous decision-making support. SAVE is a modeling tool suite to specify, analyze, verify and evaluate a varied set of requirements for DM-RTSs (Distributed Mobile Real-time Systems) with dTP-Calculus and GTS logic, currently focusing on applications in the area of smart IoT systems in smart cities. SAVE has been developed on the ADOx meta-modeling platform, with the support of the visualization capability of which all the tools of SAVE are visual, meaning that all the steps of specification, analysis, verification and evaluation are performed visually with the following components [13]:  
* Modeler--It allows the visual specification of the operational requirements of the target smart IoT system with dTP-Calculus, consisting of the ITL (In-The-Large) system and ITS (In-The-Small) process models. The ITL model defines a set of processes in the system, interconnected with a set of communication channels, and the ITS model defines a set of interactions, that is, communication and movements, with other processes in the system. The nondeterministic behavior of the processes is defined by the probability of the choice operation.
* Generator--It generates an EX (execution) model for the system from a ITL system model with its ITS process models. The EX model contains all the execution paths possible for the system. The probabilistic behavior of the system is defined by generating execution paths with probabilities, composing nondeterministic interactions between processes with probabilities.
* Simulator--It simulates any selected execution path from the EX model and generates a GTS (geo-temporal space) model. The simulation is performed probabilistically as generated by the Generator for the EX model.
* Verifier--All the SSReqs (safety and security Requirements) are specified with GTS logic and verified by the Verifier. All the requirements are verified with respect to their corresponding probabilities.
* Validator--All the SSReqs with probabilities are validated to the system probabilities. If the probabilities are not satisfied, the system improvement starts with process enhancement. If all the requirements are satisfied, we can predict that the system is reliable and sound. If not, we have to go through a sequence of steps, that is, Steps 2-1 thorough 2-6 in Figure 2, to improve the performance and capabilities of the systems until the requirements are satisfied probabilistically, based on the notions of process and system equivalences, by enhancing their corresponding probabilities to reduce respective faults or risks.  
If the requirements are not satisfied at the most enhanced levels of probabilities, the final decision can be made that the system cannot satisfy the requirements probabilistically with any means of upgrading the equivalent processes and their corresponding system.