{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T23:23:44Z","timestamp":1781306624917,"version":"3.54.1"},"reference-count":37,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2024,1,24]],"date-time":"2024-01-24T00:00:00Z","timestamp":1706054400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"publisher","award":["NRF-2022K1A3A1A18079935"],"award-info":[{"award-number":["NRF-2022K1A3A1A18079935"]}],"id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sensors"],"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.3390\/s24030767","type":"journal-article","created":{"date-parts":[[2024,1,24]],"date-time":"2024-01-24T09:57:42Z","timestamp":1706090262000},"page":"767","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Process Algebraic Approach for Probabilistic Verification of Safety and Security Requirements of Smart IoT (Internet of Things) Systems in Digital Twin"],"prefix":"10.3390","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2167-9222","authenticated-orcid":false,"given":"Junsup","family":"Song","sequence":"first","affiliation":[{"name":"Department of Computer Science and Engineering, Jeonbuk National University, Jeonju 561-756, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sunghyun","family":"Lee","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, Jeonbuk National University, Jeonju 561-756, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dimitris","family":"Karagiannis","sequence":"additional","affiliation":[{"name":"Research Group Knowledge Engineering, University of Vienna, 1010 Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2541-3066","authenticated-orcid":false,"given":"Moonkun","family":"Lee","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, Jeonbuk National University, Jeonju 561-756, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"1968","published-online":{"date-parts":[[2024,1,24]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1504\/IJPD.2005.006669","article-title":"Product lifecycle management: The new paradigm for enterprises","volume":"2","author":"Grieves","year":"2005","journal-title":"Int. J. Prod. Dev."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1109\/MSMC.2017.2702391","article-title":"The internet of things in manufacturing: Key issues and potential applications","volume":"4","author":"Yang","year":"2018","journal-title":"IEEE Syst. Man Cybern. Mag."},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"2405","DOI":"10.1109\/TII.2018.2873186","article-title":"Digital twin in industry: State-of-the-art","volume":"15","author":"Tao","year":"2018","journal-title":"IEEE Trans. Ind. Inform."},{"key":"ref_4","first-page":"100074","article-title":"Machine Learning based quality prediction for milling processes using internal machine tool data","volume":"4","author":"Fertig","year":"2022","journal-title":"Adv. Ind. Manuf. Eng."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"314","DOI":"10.1016\/0263-2373(88)90033-3","article-title":"Servitization of business: Adding value by adding services","volume":"6","author":"Vandermerwe","year":"1988","journal-title":"Eur. Manag. J."},{"key":"ref_6","unstructured":"Bumann, A. (2022). Navigating the Black Box: Generativity and Incongruences in Digital Innovation, Technical Report, Chalmers Tekniska Hogskola."},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"4541","DOI":"10.1109\/TITS.2022.3167650","article-title":"AI-empowered speed extraction via port-like videos for vehicular trajectory analysis","volume":"24","author":"Chen","year":"2022","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"48","DOI":"10.23919\/JCIN.2022.9745481","article-title":"Adaptive digital twin for vehicular edge computing and networks","volume":"7","author":"Dai","year":"2022","journal-title":"J. Commun. Inf. Netw."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"490","DOI":"10.1038\/d41586-019-02849-1","article-title":"Make more digital twins","volume":"573","author":"Tao","year":"2019","journal-title":"Nature"},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"030901","DOI":"10.1115\/1.4046739","article-title":"Digital twins: State-of-the-art and future directions for modeling and simulation in engineering dynamics applications","volume":"6","author":"Wagg","year":"2020","journal-title":"ASCE-ASME J. Risk Uncertain. Eng. Syst. Part B Mech. Eng."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1186\/s40323-020-00147-4","article-title":"How to tell the difference between a model and a digital twin","volume":"7","author":"Wright","year":"2020","journal-title":"Adv. Model. Simul. Eng. Sci."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"1141","DOI":"10.1007\/s12652-018-0911-3","article-title":"An application framework of digital twin and its case study","volume":"10","author":"Zheng","year":"2019","journal-title":"J. Ambient. Intell. Humaniz. Comput."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"103763","DOI":"10.1016\/j.compind.2022.103763","article-title":"Digital twins: An analysis framework and open issues","volume":"143","author":"Boyes","year":"2022","journal-title":"Comput. Ind."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/j.cogr.2023.04.003","article-title":"Digital Twin applications toward Industry 4.0: A Review","volume":"3","author":"Javaid","year":"2023","journal-title":"Cogn. Robot."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1016\/j.bmt.2023.02.001","article-title":"Exploring the revolution in healthcare systems through the applications of digital twin technology","volume":"4","author":"Haleem","year":"2023","journal-title":"Biomed. Technol."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"11080","DOI":"10.1109\/TII.2023.3242806","article-title":"Efficient control representation in Digital Twins: An imperative challenge for declarative languages","volume":"19","author":"Cimino","year":"2023","journal-title":"IEEE Trans. Ind. Informatics"},{"key":"ref_17","unstructured":"Wright, T., Gomes, C., and Woodcock, J. (2022). International Symposium on Leveraging Applications of Formal Methods, Springer Nature."},{"key":"ref_18","unstructured":"Song, J., and Lee, M. (2019). IFIP Working Conference on The Practice of Enterprise Modeling, Springer."},{"key":"ref_19","unstructured":"Song, J., Choe, Y., and Lee, M. (2019). International Conference on Knowledge Science, Engineering and Management, Springer."},{"key":"ref_20","unstructured":"Pressman, R.S. (2005). Software Engineering: A Practitioner\u2019s Approach, Palgrave Macmillan."},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Song, J., Karagiannis, D., and Lee, M. (2022). Modeling Method to Abstract Collective Behavior of Smart IoT Systems in CPS. Sensor, 22.","DOI":"10.3390\/s22135057"},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Karagiannis, D., Mayr, H.C., and Mylopoulos, J. (2016). Domain-Specific Conceptual Modeling: Concepts, Methods and Tools, Springer International Publishing.","DOI":"10.1007\/978-3-319-39417-6"},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Karagiannis, D., Lee, M., Hinkelmann, K., and Utz, W. (2022). Domain-Specific Conceptual Modeling: Concepts, Methods and ADOxx Tools, Springer Nature.","DOI":"10.1007\/978-3-030-93547-4"},{"key":"ref_24","unstructured":"OMiLAB (2023, November 10). OMiLAB NPO. Available online: https:\/\/www.omilab.org."},{"key":"ref_25","unstructured":"Muck, C., and Palkovits-Rauter, S. (2021). Domain-Specific Conceptual Modeling: Concepts, Methods and ADOxx Tools, Springer International Publishing."},{"key":"ref_26","unstructured":"Morita, T., and Yamaguchi, T. (2021). Domain-Specific Conceptual Modeling: Concepts, Methods and ADOxx Tools, Springer International Publishing."},{"key":"ref_27","unstructured":"(2023, November 11). SAVE v3.0. Available online: https:\/\/austria.omilab.org\/psm\/content\/save\/info."},{"key":"ref_28","unstructured":"(2023, November 11). OMiLAB NPO: MM-DSL toolkit: CoChaCo. Available online: https:\/\/www.omilab.org\/activities\/cochaco.html."},{"key":"ref_29","unstructured":"(2023, November 15). ADOxx Building Block. Available online: https:\/\/www.adoxx.org\/live\/building-blocks."},{"key":"ref_30","unstructured":"(2023, November 15). NodeJS. Available online: https:\/\/nodejs.org\/en\/learn\/getting-started\/introduction-to-nodejs."},{"key":"ref_31","unstructured":"(2023, November 15). Json. Available online: https:\/\/www.json.org\/json-en.html."},{"key":"ref_32","unstructured":"(2023, November 15). Arduino. Available online: https:\/\/www.arduino.cc."},{"key":"ref_33","unstructured":"Feng, C., and Hillston, J. (2014). International Conference on Quantitative Evaluation of Systems, Springer."},{"key":"ref_34","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1016\/j.jlap.2007.02.005","article-title":"Resources in process algebra","volume":"72","author":"Lee","year":"2007","journal-title":"J. Log. Algebr. Program."},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1109\/5.259433","article-title":"A process algebraic approach to the specification and analysis of resource-bound real-time systems","volume":"82","author":"Lee","year":"1994","journal-title":"Proc. IEEE"},{"key":"ref_36","unstructured":"Hansson, H.A. (1994). Time and probability in formal design of distributed systems. [Ph.D. Thesis, Dept. of Computer Systems, Uppsala University]."},{"key":"ref_37","doi-asserted-by":"crossref","unstructured":"Milner, R. (1980). A Calculus of Communicating Systems, Springer.","DOI":"10.1007\/3-540-10235-3"}],"container-title":["Sensors"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1424-8220\/24\/3\/767\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T13:48:46Z","timestamp":1760104126000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1424-8220\/24\/3\/767"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,24]]},"references-count":37,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2024,2]]}},"alternative-id":["s24030767"],"URL":"https:\/\/doi.org\/10.3390\/s24030767","relation":{},"ISSN":["1424-8220"],"issn-type":[{"value":"1424-8220","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,24]]}}}