{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:49:46Z","timestamp":1757314186103},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030255428"},{"type":"electronic","value":"9783030255435"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-25543-5_28","type":"book-chapter","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T12:03:09Z","timestamp":1562932989000},"page":"496-514","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Integrating Formal Schedulability Analysis into a Verified OS Kernel"],"prefix":"10.1007","author":[{"given":"Xiaojie","family":"Guo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maxime","family":"Lesourd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mengqi","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lionel","family":"Rieg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-319-43144-4_4","volume-title":"Interactive Theorem Proving","author":"J Andronick","year":"2016","unstructured":"Andronick, J., Lewis, C., Matichuk, D., Morgan, C., Rizkallah, C.: Proof of OS scheduling behavior in the presence of interrupt-induced concurrency. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 52\u201368. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-43144-4_4"},{"doi-asserted-by":"crossref","unstructured":"Andronick, J., Lewis, C., Morgan, C.: Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system. In: Proceedings Workshop on Models for Formal Analysis of Real Systems, MARS, pp. 10\u201324 (2015). \n                      https:\/\/doi.org\/10.4204\/EPTCS.196.2","key":"28_CR2","DOI":"10.4204\/EPTCS.196.2"},{"doi-asserted-by":"crossref","unstructured":"Baruah, S.: Techniques for multiprocessor global schedulability analysis. In: Proceedings - 28th IEEE International Real-Time Systems Symposium (RTSS), pp. 119\u2013128, December 2007. \n                      https:\/\/doi.org\/10.1109\/RTSS.2007.35","key":"28_CR3","DOI":"10.1109\/RTSS.2007.35"},{"doi-asserted-by":"crossref","unstructured":"Bertogna, M., Cirinei, M.: Response-time analysis for globally scheduled symmetric multiprocessor platforms. In: 28th IEEE International Real-Time Systems Symposium (RTSS), pp. 149\u2013160, December 2007. \n                      https:\/\/doi.org\/10.1109\/RTSS.2007.31","key":"28_CR4","DOI":"10.1109\/RTSS.2007.31"},{"issue":"11","key":"28_CR5","doi-asserted-by":"publisher","first-page":"1462","DOI":"10.1109\/TC.2004.103","volume":"53","author":"E Bini","year":"2004","unstructured":"Bini, E., Buttazzo, G.C.: Schedulability analysis of periodic fixed priority systems. IEEE Trans. Comput. 53(11), 1462\u20131473 (2004)","journal-title":"IEEE Trans. Comput."},{"doi-asserted-by":"crossref","unstructured":"Blackham, B., Shi, Y., Chattopadhyay, S., Roychoudhury, A., Heiser, G.: Timing analysis of a protected operating system kernel. In: 2011 IEEE 32nd Real-Time Systems Symposium (RTSS), pp. 339\u2013348, November 2011. \n                      https:\/\/doi.org\/10.1109\/RTSS.2011.38","key":"28_CR6","DOI":"10.1109\/RTSS.2011.38"},{"doi-asserted-by":"crossref","unstructured":"Cerqueira, F., Stutz, F., Brandenburg, B.B.: PROSA: a case for readable mechanized schedulability analysis. In: 28th Euromicro Conference on Real-Time Systems (ECRTS), pp. 273\u2013284 (2016). \n                      https:\/\/doi.org\/10.1109\/ECRTS.2016.28","key":"28_CR7","DOI":"10.1109\/ECRTS.2016.28"},{"unstructured":"Cordovilla, M., Boniol, F., Noulard, E., Pagetti, C.: Multiprocessor schedulability analyser. In: Proceedings of the 2011 ACM Symposium on Applied Computing, SAC 2011, pp. 735\u2013741 (2011). \n                      http:\/\/doi.acm.org\/10.1145\/1982185.1982345","key":"28_CR8"},{"unstructured":"Costanzo, D., Shao, Z., Gu, R.: End-to-end verification of information-flow security for C and assembly programs. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 648\u2013664 (2016). \n                      http:\/\/doi.acm.org\/10.1145\/2908080.2908100","key":"28_CR9"},{"unstructured":"Dutertre, B.: The priority ceiling protocol: formalization and analysis using PVS. In: Proceedings of the 21st IEEE Conference on Real-Time Systems Symposium (RTSS), pp. 151\u2013160 (1999)","key":"28_CR10"},{"key":"28_CR11","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1016\/j.jss.2017.12.033","volume":"138","author":"T Feld","year":"2018","unstructured":"Feld, T., Biondi, A., Davis, R.I., Buttazzo, G.C., Slomka, F.: A survey of schedulability analysis techniques for rate-dependent tasks. J. Syst. Softw. 138, 100\u2013107 (2018). \n                      https:\/\/doi.org\/10.1016\/j.jss.2017.12.033","journal-title":"J. Syst. Softw."},{"issue":"2","key":"28_CR12","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/j.tcs.2005.11.019","volume":"354","author":"E Fersman","year":"2006","unstructured":"Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Schedulability analysis of fixed-priority systems using timed automata. Theor. Comput. Sci. 354(2), 301\u2013317 (2006)","journal-title":"Theor. Comput. Sci."},{"unstructured":"Gu, R., et al.: Deep specifications and certified abstraction layers. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 595\u2013608 (2015). \n                      http:\/\/doi.acm.org\/10.1145\/2676726.2676975","key":"28_CR13"},{"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), pp. 653\u2013669. USENIX Association (2016). \n                      https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu","key":"28_CR14"},{"unstructured":"Gu, R., et al.: Certified concurrent abstraction layers. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 646\u2013661 (2018). \n                      http:\/\/doi.acm.org\/10.1145\/3192366.3192381","key":"28_CR15"},{"doi-asserted-by":"crossref","unstructured":"Guan, N., Gu, Z., Deng, Q., Gao, S., Yu, G.: Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking. In: IFIP International Workshop on Software Technolgies for Embedded and Ubiquitous Systems, pp. 263\u2013272 (2007)","key":"28_CR16","DOI":"10.1007\/978-3-540-75664-4_26"},{"doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP), pp. 207\u2013220 (2009). \n                      https:\/\/doi.org\/10.1145\/1629575.1629596","key":"28_CR17","DOI":"10.1145\/1629575.1629596"},{"issue":"2\u20134","key":"28_CR18","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-009-9126-9","volume":"42","author":"G Klein","year":"2009","unstructured":"Klein, G., Huuck, R., Schlich, B.: Operating system verification. J. Autom. Reasoning 42(2\u20134), 123\u2013124 (2009). \n                      https:\/\/doi.org\/10.1007\/s10817-009-9126-9","journal-title":"J. Autom. Reasoning"},{"key":"28_CR19","volume-title":"Microc\/OS-II","author":"JJ Labrosse","year":"1998","unstructured":"Labrosse, J.J.: Microc\/OS-II, 2nd edn. R&D Books, Gilroy (1998)","edition":"2"},{"issue":"1","key":"28_CR20","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/321738.321743","volume":"20","author":"CL Liu","year":"1973","unstructured":"Liu, C.L., Layland, J.W.: Scheduling algorithms for multiprogramming in a hard-real-time environment. J. ACM (JACM) 20(1), 46\u201361 (1973)","journal-title":"J. ACM (JACM)"},{"unstructured":"Liu, M., et al.: Compositional verification of preemptive OS kernels with temporal and spatial isolation. Technical report, YALEU\/DCS\/TR-1549. Department of Computer Science, Yale University (2019)","key":"28_CR21"},{"doi-asserted-by":"crossref","unstructured":"Nelson, L., et al.: Hyperkernel: push-button verification of an OS kernel. In: Proceedings of the 26th Symposium on Operating Systems Principles (SOSP), Shanghai, China, 28\u201331 October 2017, pp. 252\u2013269 (2017). \n                      https:\/\/doi.org\/10.1145\/3132747.3132748","key":"28_CR22","DOI":"10.1145\/3132747.3132748"},{"unstructured":"Palencia, J.C., Harbour, M.G.: Schedulability analysis for tasks with static and dynamic offsets. In: Proceedings 19th IEEE Real-Time Systems Symposium (RTSS), pp. 26\u201337. IEEE (1998)","key":"28_CR23"},{"issue":"5","key":"28_CR24","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1007\/s11241-017-9286-3","volume":"53","author":"T Sewell","year":"2017","unstructured":"Sewell, T., Kam, F., Heiser, G.: High-assurance timing analysis for a high-assurance real-time operating system. Real-Time Syst. 53(5), 812\u2013853 (2017). \n                      https:\/\/doi.org\/10.1007\/s11241-017-9286-3","journal-title":"Real-Time Syst."},{"unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual. INRIA, 8.4pl4 edn. (2014). \n                      https:\/\/coq.inria.fr\/distrib\/8.4pl4\/files\/Reference-Manual.pdf","key":"28_CR25"},{"unstructured":"Tindell, K., Burns, A.: Guaranteeing message latencies on controller area network (CAN). In: Proceedings of 1st International CAN Conference, pp. 1\u201311 (1994)","key":"28_CR26"},{"issue":"8","key":"28_CR27","doi-asserted-by":"publisher","first-page":"1163","DOI":"10.1016\/0967-0661(95)00112-8","volume":"3","author":"K Tindell","year":"1995","unstructured":"Tindell, K., Burns, A., Wellings, A.: Calculating controller area network (CAN) message response times. Control Eng. Pract. 3(8), 1163\u20131169 (1995)","journal-title":"Control Eng. Pract."},{"issue":"2\u20133","key":"28_CR28","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0165-6074(94)90080-9","volume":"40","author":"K Tindell","year":"1994","unstructured":"Tindell, K., Clark, J.: Holistic schedulability analysis for distributed hard real-time systems. Microprocessing Microprogramming 40(2\u20133), 117\u2013134 (1994)","journal-title":"Microprocessing Microprogramming"},{"doi-asserted-by":"crossref","unstructured":"Tindell, K., Hanssmon, H., Wellings, A.J.: Analysing real-time communications: controller area network (CAN). In: Proceedings of the 15th IEEE Real-Time Systems Symposium (RTSS), San Juan, Puerto Rico, 7\u20139 December 1994, pp. 259\u2013263 (1994). \n                      https:\/\/doi.org\/10.1109\/REAL.1994.342710","key":"28_CR29","DOI":"10.1109\/REAL.1994.342710"},{"doi-asserted-by":"crossref","unstructured":"Wilding, M.: A machine-checked proof of the optimality of a real-time scheduling policy. In: Proceedings of the 10th International Conference on Computer Aided Verification (CAV), pp. 369\u2013378 (1998)","key":"28_CR30","DOI":"10.1007\/BFb0028759"},{"key":"28_CR31","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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-41540-6_4"},{"issue":"3","key":"28_CR32","first-page":"173","volume":"14","author":"Q Xu","year":"2008","unstructured":"Xu, Q., Zhan, N.: Formalising scheduling theories in duration calculus. Nord. J. Comput. 14(3), 173\u2013201 (2008)","journal-title":"Nord. J. Comput."},{"doi-asserted-by":"crossref","unstructured":"Yuhua, Z., Chaochen, Z.: A formal proof of the deadline driven scheduler. In: International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 756\u2013775 (1994)","key":"28_CR33","DOI":"10.1007\/3-540-58468-4_194"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-25543-5_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T12:10:38Z","timestamp":1562933438000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-25543-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030255428","9783030255435"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-25543-5_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York City, NY","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav0","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"258","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}