{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:15:04Z","timestamp":1783545304416,"version":"3.55.0"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    OpenHarmony LiteOS-M, a preemptive operating system (OS) kernel for the Internet of Things (IoT), is widely deployed in safety-critical domains, such as aerospace and transportation. As a rigorous method to assure software safety, formal verification has been applied to OS kernels in industry. However, entirely verified kernels with large codebases are rare, since such verification is typically performed within interactive theorem provers, requiring substantial human effort. In this paper, we present the\n                    <jats:italic>functional correctness<\/jats:italic>\n                    verification of LiteOS-M. First, to improve verification efficiency, we design a formal verification platform, Smart Verifier. The platform employs an annotation-based verifier as the front end, while the back end integrates Z3 and Rocq, combining automatic and interactive theorem proving techniques. Second, we tailor two verification methods, expressing program refinement as standard Hoare logic triples and modeling concurrency through state transition systems, to utilize the platform for verifying LiteOS-M. Our verified LiteOS-M kernel consists of 17,000 lines of C. During the code review and verification, we find a total of 17 bugs, all confirmed and fixed by developers.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_32","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:21:28Z","timestamp":1779024088000},"page":"651-669","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of\u00a0Functional Correctness for\u00a0the\u00a0OpenHarmony LiteOS-M Kernel"],"prefix":"10.1007","author":[{"given":"Tianqi","family":"Zhao","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qinxiang","family":"Cao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shenghua","family":"Feng","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Minghui","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yongzhi","family":"Cao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Junfeng","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Haiyan","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hao","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhenjiang","family":"Hu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. In: Proceedings of the Third Annual Symposium on Logic in Computer Science, LICS \u201988, Edinburgh, Scotland, UK, 5\u20138 July 1988, pp. 165\u2013175. IEEE Computer Society (1988)","DOI":"10.1109\/LICS.1988.5115"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., et al.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2"},{"key":"32_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"1","key":"32_CR5","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1145\/2775051.2676975","volume":"50","author":"R Gu","year":"2015","unstructured":"Gu, R., et al.: Deep specifications and certified abstraction layers. ACM SIGPLAN Not. 50(1), 595\u2013608 (2015)","journal-title":"ACM SIGPLAN Not."},{"key":"32_CR6","unstructured":"Gu, R., et al.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), pp. 653\u2013669 (2016)"},{"issue":"6","key":"32_CR7","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein, G., et al.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010)","journal-title":"Commun. ACM"},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1007\/978-3-642-05089-3_51","volume-title":"FM 2009: Formal Methods","author":"D Leinenbach","year":"2009","unstructured":"Leinenbach, D., Santen, T.: Verifying the Microsoft Hyper-V Hypervisor with VCC. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 806\u2013809. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-05089-3_51"},{"key":"32_CR9","unstructured":"OpenAtom Foundation: OpenHarmony Official Website (2020). https:\/\/www.openharmony.cn"},{"key":"32_CR10","doi-asserted-by":"crossref","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, pp. 377\u2013390 (2013)","DOI":"10.1145\/2500365.2500600"},{"issue":"1","key":"32_CR11","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1145\/2480359.2429111","volume":"48","author":"AJ Turon","year":"2013","unstructured":"Turon, A.J., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical relations for fine-grained concurrency. ACM SIGPLAN Not. 48(1), 343\u2013356 (2013)","journal-title":"ACM SIGPLAN Not."},{"key":"32_CR12","unstructured":"Wang, Z., et al.: Stellis: a strategy language for purifying separation logic entailments. arXiv preprint arXiv:2512.05159 (2025)"},{"issue":"OOPSLA2","key":"32_CR13","doi-asserted-by":"publisher","first-page":"2454","DOI":"10.1145\/3763138","volume":"9","author":"S Wu","year":"2025","unstructured":"Wu, S., Wu, X., Cao, Q.: Encode the $$\\forall $$$$\\exists $$ relational Hoare logic into standard Hoare logic. Proce. ACM Program. Lang. 9(OOPSLA2), 2454\u20132481 (2025)","journal-title":"Proce. ACM Program. Lang."},{"key":"32_CR14","unstructured":"Wu, X., et\u00a0al.: QCP: a practical separation logic-based c program verification tool. arXiv preprint arXiv:2505.12878 (2025)"},{"key":"32_CR15","unstructured":"Wu, Y., Xia, B., Xu, J., Zhan, B., Zhao, T.: OSVAuto: automatic proofs about functional specifications in OS verification. arXiv preprint arXiv:2403.13457 (2024)"},{"key":"32_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-319-41540-6_4","volume-title":"Computer Aided Verification","author":"F Xu","year":"2016","unstructured":"Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z.: A practical verification framework for preemptive OS kernels. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 59\u201379. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_4"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:29:20Z","timestamp":1783542560000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}