{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:42:23Z","timestamp":1742938943401,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031150074"},{"type":"electronic","value":"9783031150081"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-15008-1_6","type":"book-chapter","created":{"date-parts":[[2022,9,4]],"date-time":"2022-09-04T23:02:47Z","timestamp":1662332567000},"page":"69-85","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Reusable Formal Models for\u00a0Custom Real-Time Operating Systems"],"prefix":"10.1007","author":[{"given":"Julius","family":"Adelt","sequence":"first","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"given":"Julian","family":"Gebker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"given":"Paula","family":"Herber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,9,5]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-46002-0_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Abdedda\u00efm","year":"2002","unstructured":"Abdedda\u00efm, Y., Maler, O.: Preemptive job-shop scheduling using stopwatch automata. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 113\u2013126. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_9"},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL \u2014 a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020949"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87\u2013124. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27755-2_3"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"B\u00e9chennec, J.L., Roux, O.H., Tigori, T.: Formal model-based conformance verification of an OSEK\/VDX compliant RTOS. In: 2018 5th International Conference on Control, Decision and Information Technologies (CoDIT), pp. 628\u2013634 (2018). https:\/\/doi.org\/10.1109\/CoDIT.2018.8394813","DOI":"10.1109\/CoDIT.2018.8394813"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Deifel, H.P., G\u00f6ttlinger, M., Milius, S., Schr\u00f6der, L., Dietrich, C., Lohmann, D.: Automatic verification of application-tailored OSEK kernels. In: IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102260"},{"key":"6_CR11","unstructured":"EV3RT Project: EV3RT (2019). https:\/\/ev3rt-git.github.io\/about\/"},{"issue":"5","key":"6_CR12","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1007\/s10009-020-00597-6","volume":"23","author":"P Han","year":"2021","unstructured":"Han, P., Zhai, Z., Nielsen, B., Nyman, U.: Model-based optimization of ARINC-653 partition scheduling. Int. J. Softw. Tools Technol. Transf. 23(5), 721\u2013740 (2021)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Herber, P., Fellmuth, J., Glesner, S.: Model checking systemc designs using timed automata. In: IEEE\/ACM\/IFIP International Conference on Hardware\/Software Codesign and System Synthesis, CODES+ISSS 2008, pp. 131\u2013136. ACM (2008). https:\/\/doi.org\/10.1145\/1450135.1450166","DOI":"10.1145\/1450135.1450166"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Huang, Y., Zhao, Y., Zhu, L., Li, Q., Zhu, H., Shi, J.: Modeling and verifying the code-level OSEK\/VDX operating system with CSP. In: 2011 Fifth International Conference on Theoretical Aspects of Software Engineering, pp. 142\u2013149. IEEE (2011)","DOI":"10.1109\/TASE.2011.11"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Klein, G., et al.: sel4: formal verification of an OS kernel. In: ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009. ACM (2009). https:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"6_CR16","doi-asserted-by":"publisher","DOI":"10.1002\/0471648299","volume-title":"Real-Time Systems Design And Analysis","author":"PA Laplante","year":"2004","unstructured":"Laplante, P.A., et al.: Real-Time Systems Design And Analysis. Wiley, New York (2004)"},{"key":"6_CR17","unstructured":"OSEK: ISO 17356\u20133:2005 Road vehicles - Open interface for embedded automotive applications - Part 3: OSEK\/VDX Operating System (OS). International Organization for Standardization (2005)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Shi, J., He, J., Zhu, H., Fang, H., Huang, Y., Zhang, X.: ORIENTAIS: Formal verified OSEK\/VDX real-time operating system. In: 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems. pp. 293\u2013301. IEEE (2012)","DOI":"10.1109\/ICECCS20050.2012.6299224"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Tigori, K.T.G., B\u00e9chennec, J.L., Faucou, S., Roux, O.H.: Formal model-based synthesis of application-specific static rtos. ACM Trans. Embed. Comput. Syst. 16(4), 1\u201325 (017). https:\/\/doi.org\/10.1145\/3015777","DOI":"10.1145\/3015777"},{"key":"6_CR20","unstructured":"TOPPERS Project: Toyohashi open platform for embedded real-time systems. https:\/\/www.toppers.jp\/en\/project.html"},{"key":"6_CR21","unstructured":"TRON: $$\\mu $$ITRON4.0 Specification (2007). https:\/\/www.tron.org\/wp-content\/themes\/dp-magjam\/pdf\/specifications\/en_US\/TEF024-S001-04.03.00_en.pdf. Accessed 02 Sep 2021"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Vu, D.H., Chiba, Y., Yatake, K., Aoki, T.: Verifying OSEK\/VDX OS design using its formal specification. In: 2016 10th International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 81\u201388. IEEE (2016)","DOI":"10.1109\/TASE.2016.18"},{"issue":"1","key":"6_CR23","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s11241-007-9036-z","volume":"38","author":"L Waszniowski","year":"2008","unstructured":"Waszniowski, L., Hanz\u00e1lek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38(1), 39\u201365 (2008)","journal-title":"Real-Time Syst."},{"issue":"10","key":"6_CR24","doi-asserted-by":"publisher","first-page":"1765","DOI":"10.1587\/transinf.2015EDP7043","volume":"98","author":"H Zhang","year":"2015","unstructured":"Zhang, H., Aoki, T., Chiba, Y.: Verifying OSEK\/VDX applications: a sequentialization-based model checking approach. IEICE Trans. Inf. Sys. 98(10), 1765\u20131776 (2015)","journal-title":"IEICE Trans. Inf. Sys."},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Zhang, H., Aoki, T., Lin, H.H., Zhang, M., Chiba, Y., Yatake, K.: SMT-based bounded model checking for OSEK\/VDX applications. In: 2013 20th Asia-Pacific Software Engineering Conference (APSEC), vol. 1, pp. 307\u2013314. IEEE (2013)","DOI":"10.1109\/APSEC.2013.49"},{"issue":"3","key":"6_CR26","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1662","volume":"28","author":"H Zhang","year":"2018","unstructured":"Zhang, H., Li, G., Cheng, Z., Xue, J.: Verifying OSEK\/VDX automotive applications: a spin-based model checking approach. Softw. Test. Verif. Reliab. 28(3), e1662 (2018)","journal-title":"Softw. Test. Verif. Reliab."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-15008-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,4]],"date-time":"2022-09-04T23:09:16Z","timestamp":1662332956000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-15008-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031150074","9783031150081"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-15008-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"5 September 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Warsaw","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Poland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2022","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":"fmics2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fmics2022.fsa.win.tue.nl\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"22","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":"13","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":"59% - 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":"2.5","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}