{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:28:30Z","timestamp":1772836110149,"version":"3.50.1"},"reference-count":35,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"9","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2023,9,1]]},"DOI":"10.1587\/transinf.2022edp7223","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T23:08:32Z","timestamp":1693523312000},"page":"1507-1518","source":"Crossref","is-referenced-by-count":3,"title":["IoT Modeling and Verification: From the CaIT Calculus to UPPAAL"],"prefix":"10.1587","volume":"E106.D","author":[{"given":"Ningning","family":"CHEN","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"ZHU","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"publisher","unstructured":"[1] V. Araujo, K. Mitra, S. Saguna, and C. \u00c5hlund, \u201cPerformance evaluation of FIWARE: A cloud-based IoT platform for smart cities,\u201d J. Parallel Distributed Comput., vol.132, pp.250-261, Oct. 2019. 10.1016\/j.jpdc.2018.12.010","DOI":"10.1016\/j.jpdc.2018.12.010"},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] F. Alshehri and G. Muhammad, \u201cA comprehensive survey of the Internet of Things (IoT) and AI-based smart healthcare,\u201d IEEE Access, vol.9, pp.3660-3678, 2021. 10.1109\/ACCESS.2020.3047960","DOI":"10.1109\/ACCESS.2020.3047960"},{"key":"3","doi-asserted-by":"publisher","unstructured":"[3] I.U. Din, B. Ahmad, A. Almogren, H.N. Almajed, I. Mohiuddin, and J.J.P.C. Rodrigues, \u201cLeft-right-front caching strategy for vehicular networks in ICN-based Internet of Things,\u201d IEEE Access, vol.9, pp.595-605, 2021. 10.1109\/ACCESS.2020.3046887","DOI":"10.1109\/ACCESS.2020.3046887"},{"key":"4","doi-asserted-by":"crossref","unstructured":"[4] A. Krishna and G. Sala\u00fcn, \u201cBusiness process models for analysis of industrial IoT applications,\u201d IoT '21: 11th International Conference on the Internet of Things, pp.102-109, ACM, 2021. 10.1145\/3494322.3494336","DOI":"10.1145\/3494322.3494336"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] A. Krishna, M. Le Pallec, R. Mateescu, L. Noirie, and G. Sala\u00fcn, \u201cIoT Composer: Composition and deployment of IoT applications,\u201d 2019 IEEE\/ACM 41st International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), pp.19-22, 2019. 10.1109\/ICSE-Companion.2019.00028","DOI":"10.1109\/ICSE-Companion.2019.00028"},{"key":"6","doi-asserted-by":"crossref","unstructured":"[6] R. Cleaveland, A.W. Roscoe, and S.A. Smolka, \u201cProcess algebra and model checking,\u201d in Handbook of Model Checking, pp.1149-1195, Springer, 2018. 10.1007\/978-3-319-10575-8_32","DOI":"10.1007\/978-3-319-10575-8_32"},{"key":"7","unstructured":"[7] J.A. Bergstra, A. Ponse, and S.A. Smolka, eds., Handbook of Process Algebra, North-Holland \/ Elsevier, 2001. 10.1016\/B978-044482830-9\/50017-5"},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] A. Fehnker, R. van Glabbeek, P. H\u00f6fner, A. McIver, M. Portmann, and W.L. Tan, \u201cAutomated analysis of aodv using uppaal,\u201d TACAS, pp.173-187, Springer, 2012. 10.1007\/978-3-642-28756-5_13","DOI":"10.1007\/978-3-642-28756-5_13"},{"key":"9","unstructured":"[9] D.M. Jackson, Logical verification of reactive software systems, Ph.D. thesis, University of Oxford, UK, 1992."},{"key":"10","unstructured":"[10] J. Ouaknine and J. Worrell, \u201cTimed CSP =closed timed epsilon-automata,\u201d Nord. J. Comput., vol.10, no.2, pp.99-133, 2003."},{"key":"11","doi-asserted-by":"crossref","unstructured":"[11] I. Lanese, L. Bedogni, and M.D. Felice, \u201cInternet of things: a process calculus approach,\u201d Proc. 28th Annual ACM Symposium on Applied Computing, pp.1339-1346, ACM, March 2013. 10.1145\/2480362.2480615","DOI":"10.1145\/2480362.2480615"},{"key":"12","doi-asserted-by":"publisher","unstructured":"[12] R. Lanotte and M. Merro, \u201cA semantic theory of the Internet of Things,\u201d Inf. Comput., vol.259, no.1, pp.72-101, April 2018. 10.1016\/j.ic.2018.01.001","DOI":"10.1016\/j.ic.2018.01.001"},{"key":"13","doi-asserted-by":"publisher","unstructured":"[13] K.V.S. Prasad, \u201cA calculus of broadcasting systems,\u201d Sci. Comput. Program., vol.25, no.2-3, pp.285-327, Dec. 1995. 10.1016\/0167-6423(95)00017-8","DOI":"10.1016\/0167-6423(95)00017-8"},{"key":"14","doi-asserted-by":"crossref","unstructured":"[14] C. Ene and T. Muntean, \u201cA broadcast-based calculus for communicating systems,\u201d Proceedings 15th International Parallel and Distributed Processing Symposium. IPDPS 2001, pp.1516-1525, 2001. 10.1109\/IPDPS.2001.925136","DOI":"10.1109\/IPDPS.2001.925136"},{"key":"15","doi-asserted-by":"publisher","unstructured":"[15] S. Nanz and C. Hankin, \u201cA framework for security analysis of mobile wireless networks,\u201d Theor. Comput. Sci., vol.367, no.1-2, pp.203-227, Nov. 2006. 10.1016\/j.tcs.2006.08.036","DOI":"10.1016\/j.tcs.2006.08.036"},{"key":"16","doi-asserted-by":"publisher","unstructured":"[16] I. Lanese and D. Sangiorgi, \u201cAn operational semantics for a calculus for wireless systems,\u201d Theor. Comput. Sci., vol.411, no.19, pp.1928-1948, April 2010. 10.1016\/j.tcs.2010.01.023","DOI":"10.1016\/j.tcs.2010.01.023"},{"key":"17","doi-asserted-by":"publisher","unstructured":"[17] A. Singh, C.R. Ramakrishnan, and S.A. Smolka, \u201cA process calculus for mobile ad hoc networks,\u201d Sci. Comput. Program., vol.75, no.6, pp.440-469, June 2010. 10.1016\/j.scico.2009.07.008","DOI":"10.1016\/j.scico.2009.07.008"},{"key":"18","unstructured":"[18] C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall, 1985."},{"key":"19","doi-asserted-by":"publisher","unstructured":"[19] B. Aman and G. Ciobanu, \u201cReal-time migration properties of rTiMo verified in Uppaal,\u201d Software Engineering and Formal Methods-11th International Conference, SEFM 2013, pp.31-45, Springer, 2013. 10.1007\/978-3-642-40561-7_3","DOI":"10.1007\/978-3-642-40561-7_3"},{"key":"20","doi-asserted-by":"publisher","unstructured":"[20] S. Cattani and M.Z. Kwiatkowska, \u201cA refinement-based process algebra for timed automata,\u201d Formal Aspects Comput., vol.17, no.2, pp.138-159, Aug. 2005. 10.1007\/s00165-005-0064-y","DOI":"10.1007\/s00165-005-0064-y"},{"key":"21","doi-asserted-by":"publisher","unstructured":"[21] R. Alur and D.L. Dill, \u201cA theory of timed automata,\u201d Theor. Comput. Sci., vol.126, no.2, pp.183-235, April 1994. 10.1016\/0304-3975(94)90010-8","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"22","doi-asserted-by":"crossref","unstructured":"[22] G. Behrmann, A. David, and K.G. Larsen, \u201cA tutorial on Uppaal,\u201d SFM-RT 2004, Lect. Notes Comput. Sci., vol.3185, pp.200-236, Springer, 2004. 10.1007\/978-3-540-30080-9_7","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"23","doi-asserted-by":"crossref","unstructured":"[23] J. Bengtsson and W. Yi, \u201cTimed automata: Semantics, algorithms and tools,\u201d ACPN 2003, Lect. Notes Comput. Sci., vol.3098, pp.87-124, Springer, 2003. 10.1007\/978-3-540-27755-2_3","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"24","doi-asserted-by":"crossref","unstructured":"[24] R. Milner, J. Parrow, and D. Walker, \u201cA calculus of mobile processes, I,\u201d Inf. Comput., vol.100, no.1, pp.1-40, Sept. 1992. 10.1016\/0890-5401(92)90008-4","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"25","doi-asserted-by":"crossref","unstructured":"[25] M. Abadi and A.D. Gordon, \u201cA calculus for cryptographic protocols: The spi calculus,\u201d Inf. Comput., vol.148, no.1, pp.1-70, Jan. 1999. 10.1006\/inco.1998.2740","DOI":"10.1006\/inco.1998.2740"},{"key":"26","doi-asserted-by":"publisher","unstructured":"[26] M. Abadi, B. Blanchet, and C. Fournet, \u201cThe applied pi calculus: Mobile values, new names, and secure communication,\u201d J. ACM, vol.65, no.1, pp.1:1-1:41, Oct. 2018. 10.1145\/3127586","DOI":"10.1145\/3127586"},{"key":"27","unstructured":"[27] J. Baeten, T. Basten, and M. Reniers, Process Algebra: Equational Theories of Communicating Processes, 07 2014. 10.1017\/CBO9781139195003"},{"key":"28","doi-asserted-by":"publisher","unstructured":"[28] J. He, \u201cProcess simulation and refinement,\u201d Formal Aspects Comput., vol.1, no.3, pp.229-241, March 1989. 10.1007\/BF01887207","DOI":"10.1007\/BF01887207"},{"key":"29","doi-asserted-by":"publisher","unstructured":"[29] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, \u201cSymbolic model checking for real-time systems,\u201d Inf. Comput., vol.111, no.2, pp.193-244, June 1994. 10.1006\/inco.1994.1045","DOI":"10.1006\/inco.1994.1045"},{"key":"30","doi-asserted-by":"crossref","unstructured":"[30] S. Liu and N. Yoshiura, \u201cModel checking of TTCAN protocol using UPPAAL,\u201d Computational Science and Its Applications-ICCSA 2018, Lect. Notes Comput. Sci., vol.10963, pp.550-564, Springer, July 2018. 10.1007\/978-3-319-95171-3_43","DOI":"10.1007\/978-3-319-95171-3_43"},{"key":"31","doi-asserted-by":"publisher","unstructured":"[31] K.G. Larsen, P. Pettersson, and W. Yi, \u201cUPPAAL in a nutshell,\u201d Int. J. Softw. Tools Technol. Transf., vol.1, no.1-2, pp.134-152, Feb. 1997. 10.1007\/s100090050010","DOI":"10.1007\/s100090050010"},{"key":"32","unstructured":"[32] https:\/\/github.com\/Cnn-c\/UPPAAL-and-CaIT."},{"key":"33","doi-asserted-by":"publisher","unstructured":"[33] Y. Venema, \u201cAutomata and fixed point logics for coalgebras,\u201d CMCS 2004, Electron. Notes Theor. Comput. Sci., vol.106, pp.355-375, Elsevier, Dec. 2004. 10.1016\/j.entcs.2004.02.038","DOI":"10.1016\/j.entcs.2004.02.038"},{"key":"34","doi-asserted-by":"publisher","unstructured":"[34] Y. Venema, \u201cAutomata and fixed point logic: A coalgebraic perspective,\u201d Inf. Comput., vol.204, no.4, pp.637-678, April 2006. 10.1016\/j.ic.2005.06.003","DOI":"10.1016\/j.ic.2005.06.003"},{"key":"35","doi-asserted-by":"crossref","unstructured":"[35] H.R. Nielson, F. Nielson, and R. Vigo, \u201cA calculus for quality,\u201d FACS 2012, Lect. Notes Comput. Sci., vol.7684, pp.188-204, Springer, 2012. 10.1007\/978-3-642-35861-6_12","DOI":"10.1007\/978-3-642-35861-6_12"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E106.D\/9\/E106.D_2022EDP7223\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T08:50:37Z","timestamp":1730019037000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E106.D\/9\/E106.D_2022EDP7223\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,1]]},"references-count":35,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2023]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2022edp7223","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,1]]},"article-number":"2022EDP7223"}}