{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,5]],"date-time":"2026-03-05T22:21:23Z","timestamp":1772749283479,"version":"3.50.1"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2023,9,11]],"date-time":"2023-09-11T00:00:00Z","timestamp":1694390400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,9,11]],"date-time":"2023-09-11T00:00:00Z","timestamp":1694390400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2024,4]]},"DOI":"10.1007\/s11704-022-2258-3","type":"journal-article","created":{"date-parts":[[2023,9,11]],"date-time":"2023-09-11T05:01:40Z","timestamp":1694408500000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A proof system of the CaIT calculus"],"prefix":"10.1007","volume":"18","author":[{"given":"Ningning","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,11]]},"reference":[{"issue":"7","key":"2258_CR1","first-page":"97","volume":"22","author":"K T Ashton","year":"2009","unstructured":"Ashton K. That \u201cinternet of things\u201d thing. RFID Journal, 2009, 22(7): 97\u2013114","journal-title":"RFID Journal"},{"issue":"7","key":"2258_CR2","doi-asserted-by":"publisher","first-page":"1645","DOI":"10.1016\/j.future.2013.01.010","volume":"29","author":"J Gubbi","year":"2013","unstructured":"Gubbi J, Buyya R, Marusic S, Palaniswami M. Internet of things (IoT): a vision, architectural elements, and future directions. Future Generation Computer Systems, 2013, 29(7): 1645\u20131660","journal-title":"Future Generation Computer Systems"},{"key":"2258_CR3","doi-asserted-by":"crossref","unstructured":"Zhang Y. Technology framework of the internet of things and its application. In: Proceedings of 2011 International Conference on Electrical and Control Engineering. 2011, 4109\u20134112","DOI":"10.1109\/ICECENG.2011.6057290"},{"issue":"15","key":"2258_CR4","doi-asserted-by":"publisher","first-page":"2787","DOI":"10.1016\/j.comnet.2010.05.010","volume":"54","author":"L Atzori","year":"2010","unstructured":"Atzori L, Iera A, Morabito G. The internet of things: a survey. Computer Networks, 2010, 54(15): 2787\u20132805","journal-title":"Computer Networks"},{"key":"2258_CR5","doi-asserted-by":"publisher","first-page":"85939","DOI":"10.1109\/ACCESS.2020.2992262","volume":"8","author":"M Hosseinzadeh","year":"2020","unstructured":"Hosseinzadeh M, Tho Q T, Ali S, Rahmani A M, Souri A, Norouzi M, Huynh B. A hybrid service selection and composition model for cloud-edge computing in the internet of things. IEEE Access, 2020, 8: 85939\u201385949","journal-title":"IEEE Access"},{"key":"2258_CR6","doi-asserted-by":"publisher","first-page":"113292","DOI":"10.1109\/ACCESS.2021.3103725","volume":"9","author":"Y Harbi","year":"2021","unstructured":"Harbi Y, Aliouat Z, Refoufi A, Harous S. Recent security trends in internet of things: a comprehensive survey. IEEE Access, 2021, 9: 113292\u2013113314","journal-title":"IEEE Access"},{"key":"2258_CR7","doi-asserted-by":"crossref","unstructured":"Nienhuis K, Joannou A, Bauereiss T, Fox A, Roe M, Campbell B, Naylor M, Norton R M, Moore S W, Neumann P G, Stark I, Watson R N M, Sewell P. Rigorous engineering for hardware security: formal modelling and proof in the CHERI design and implementation process. In: Proceedings of 2020 IEEE Symposium on Security and Privacy. 2020, 1003\u20131020","DOI":"10.1109\/SP40000.2020.00055"},{"key":"2258_CR8","doi-asserted-by":"crossref","unstructured":"Asavoae M, Haur I, Jan M, Ben Hedia B, Schoeberl M. Towards formal co-validation of hardware and software timing models of CPSs. In: Proceedings of the 9th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems. 2019, 203\u2013227","DOI":"10.1007\/978-3-030-41131-2_10"},{"key":"2258_CR9","unstructured":"Schmidt B. Programmnetzlisten: Ein formales Modell fur die Verifikation von Hardwarenaher Software in Eingebetteten Systemen. Technische Universitat Kaiserslautern, Dissertation, 2020"},{"key":"2258_CR10","doi-asserted-by":"crossref","unstructured":"Lanese I, Bedogni L, Di Felice M. Internet of things: a process calculus approach. In: Proceedings of the 28th Annual ACM Symposium on Applied Computing. 2013, 1339\u20131346","DOI":"10.1145\/2480362.2480615"},{"key":"2258_CR11","doi-asserted-by":"crossref","unstructured":"Bodei C, Degano P, Ferrari G L, Galletta L. Where do your IoT ingredients come from? In: Proceedings of the 18th International Conference on Coordination Languages and Models. 2016, 35\u201350","DOI":"10.1007\/978-3-319-39519-7_3"},{"key":"2258_CR12","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/j.ic.2018.01.001","volume":"259","author":"R Lanotte","year":"2018","unstructured":"Lanotte R, Merro M. A semantic theory of the internet of things. Information and Computation, 2018, 259: 72\u2013101","journal-title":"Information and Computation"},{"key":"2258_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"K R Apt","year":"2009","unstructured":"Apt K R, Olderog E R, Apt K R. Verification of Sequential and Concurrent Programs. 3rd ed. New York: Springer, 2009","edition":"3rd ed."},{"key":"2258_CR14","doi-asserted-by":"crossref","unstructured":"Hooman J. Compositional verification of real-time systems using extended Hoare triples. In: Proceedings of the Real-Time: Theory in Practice, REX Workshop. 1991, 252\u2013290","DOI":"10.1007\/BFb0031996"},{"issue":"S1","key":"2258_CR15","doi-asserted-by":"publisher","first-page":"801","DOI":"10.1007\/BF01213604","volume":"6","author":"J Hooman","year":"1994","unstructured":"Hooman J. Extending Hoare logic to real-time. Formal Aspects of Computing, 1994, 6(S1): 801\u2013825","journal-title":"Formal Aspects of Computing"},{"key":"2258_CR16","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1016\/j.phycom.2014.01.006","volume":"12","author":"I F Akyildiz","year":"2014","unstructured":"Akyildiz I F, Jornet J M, Han C. Terahertz band: next frontier for wireless communications. Physical Communication, 2014, 12: 16\u201332","journal-title":"Physical Communication"},{"key":"2258_CR17","doi-asserted-by":"publisher","DOI":"10.1002\/0470090154","volume-title":"Classification, Parameter Estimation and State Estimation: an Engineering Approach Using MATLAB","author":"F van der Heijden","year":"2004","unstructured":"van der Heijden F, Duin R P W, De Ridder D, Tax D M J. Classification, Parameter Estimation and State Estimation: an Engineering Approach Using MATLAB. Chichester: John Wiley & Sons, ltd., 2004"},{"issue":"2\u20133","key":"2258_CR18","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/0167-6423(95)00017-8","volume":"25","author":"K V S Prasad","year":"1995","unstructured":"Prasad K V S. A calculus of broadcasting systems. Science of Computer Programming, 1995, 25(2\u20133): 285\u2013327","journal-title":"Science of Computer Programming"},{"issue":"1\u20132","key":"2258_CR19","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.tcs.2006.08.036","volume":"367","author":"S Nanz","year":"2006","unstructured":"Nanz S, Hankin C. A framework for security analysis of mobile wireless networks. Theoretical Computer Science, 2006, 367(1\u20132): 203\u2013227","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"2258_CR20","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/j.ic.2007.11.010","volume":"207","author":"M Merro","year":"2009","unstructured":"Merro M. An observational theory for mobile ad hoc networks (full version). Information and Computation, 2009, 207(2): 194\u2013208","journal-title":"Information and Computation"},{"issue":"10","key":"2258_CR21","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C A R Hoare","year":"1969","unstructured":"Hoare C A R. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576\u2013580","journal-title":"Communications of the ACM"},{"key":"2258_CR22","doi-asserted-by":"crossref","unstructured":"Barthe G, Gaboardi M, Arias E J G, Hsu J, Kunz C, Strub P Y. Proving differential privacy in Hoare logic. In: Proceedings of the 27th IEEE Computer Security Foundations Symposium. 2014, 411\u2013424","DOI":"10.1109\/CSF.2014.36"},{"issue":"3","key":"2258_CR23","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/s00165-011-0180-9","volume":"25","author":"R Arthan","year":"2013","unstructured":"Arthan R, Martin U, Oliva P. A Hoare logic for linear systems. Formal Aspects of Computing, 2013, 25(3): 345\u2013363","journal-title":"Formal Aspects of Computing"},{"issue":"4","key":"2258_CR24","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/s11704-008-0039-2","volume":"2","author":"C Luo","year":"2008","unstructured":"Luo C, Qin S, Qiu Z. Verifying BPEL-like programs with Hoare logic. Frontiers of Computer Science in China, 2008, 2(4): 344\u2013356","journal-title":"Frontiers of Computer Science in China"},{"issue":"1\u20132","key":"2258_CR25","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00304-2","volume":"274","author":"F S de Boer","year":"2002","unstructured":"de Boer F S. A Hoare logic for dynamic networks of asynchronously communicating deterministic processes. Theoretical Computer Science, 2002, 274(1\u20132): 3\u201341","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"2258_CR26","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/357103.357110","volume":"2","author":"K R Apt","year":"1980","unstructured":"Apt K R, Francez N, de Roever W P. A proof system for communicating sequential processes. ACM Transactions on Programming Languages and Systems, 1980, 2(3): 359\u2013385","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2258_CR27","volume-title":"Unifying Theories of Programming","author":"C A R Hoare","year":"1998","unstructured":"Hoare C A R, He J. Unifying Theories of Programming. London: Prentice Hall, 1998"},{"key":"2258_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: a Generic Theorem Prover","author":"L C Paulson","year":"1994","unstructured":"Paulson L C. Isabelle: a Generic Theorem Prover. Berlin: Springer, 1994"},{"key":"2258_CR29","unstructured":"Huet G, Kahn G, Paulin-Mohring C. The coq proof assistant: a tutorial. Rapport Technique, 1997, 178"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-022-2258-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11704-022-2258-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-022-2258-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,11]],"date-time":"2023-09-11T05:05:05Z","timestamp":1694408705000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11704-022-2258-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,11]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4]]}},"alternative-id":["2258"],"URL":"https:\/\/doi.org\/10.1007\/s11704-022-2258-3","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,11]]},"assertion":[{"value":"1 May 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 December 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 September 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"182401"}}