{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T15:55:10Z","timestamp":1759938910594,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031172434"},{"type":"electronic","value":"9783031172441"}],"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-17244-1_9","type":"book-chapter","created":{"date-parts":[[2022,10,9]],"date-time":"2022-10-09T19:33:23Z","timestamp":1665344003000},"page":"140-155","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formal Verification of\u00a0the\u00a0Inter-core Synchronization of\u00a0a\u00a0Multi-core RTOS Kernel"],"prefix":"10.1007","author":[{"given":"Imane","family":"Haur","sequence":"first","affiliation":[]},{"given":"Jean-Luc","family":"B\u00e9chennec","sequence":"additional","affiliation":[]},{"given":"Olivier H.","family":"Roux","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,10,10]]},"reference":[{"key":"9_CR1","unstructured":"AUTOSAR GbR: Specification of operating system (2009)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"B\u00e9chennec, J.L., Briday, M., Faucou, S., Trinquet, Y.: Trampoline an open source implementation of the OSEK\/VDX RTOS specification. In: IEEE Conference on Emerging Technologies and Factory Automation, ETFA 2006, pp. 62\u201369 (2006)","DOI":"10.1109\/ETFA.2006.355432"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"B\u00e9chennec, J.L., Roux, O.H., Tigori, T.: Formal model-based conformance verification of an OSEK\/VDX compliant RTOS. In: International Conference on Control, Decision and Information Technologies (CODIT 2018). IEEE (2018)","DOI":"10.1109\/CoDIT.2018.8394813"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Boyer, M., Diaz, M.: Multiple enabledness of transitions in petri nets with time. In: 9th International Workshop on Petri Nets and Performance Models, PNPM 2001, pp. 219\u2013228. IEEE Computer Society (2001)","DOI":"10.1109\/PNPM.2001.953371"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Choi, Y.: Safety analysis of trampoline OS using model checking: an experience report. In: 2011 IEEE 22nd International Symposium on Software Reliability Engineering, pp. 200\u2013209 (2011)","DOI":"10.1109\/ISSRE.2011.22"},{"key":"9_CR6","unstructured":"Espinosa, T., Leon, G.: Formal verification of a real-time operating system. Master thesis, University of Saskatchewan (2012)"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Gadelha, M.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: an industrial-strength C model checker, pp. 888\u2013891. Association for Computing Machinery, New York (2018)","DOI":"10.1145\/3238147.3240481"},{"issue":"10","key":"9_CR8","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/3356903","volume":"62","author":"R Gu","year":"2019","unstructured":"Gu, R., et al.: Building certified concurrent OS kernels. Commun. ACM 62(10), 89\u201399 (2019)","journal-title":"Commun. ACM"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Haur, I., B\u00e9chennec, J.L., Roux, O.H.: High-level colored time petri nets for true concurrency modeling in real-time software. In: International Conference on Control, Decision and Information Technologies (CODIT 2022). IEEE (2022)","DOI":"10.1109\/CoDIT55151.2022.9803922"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Haur, I., B\u00e9chennec, J.L., Roux, O.H.: Formal schedulability analysis based on multi-core RTOS model. In: 29th International Conference on Real-Time Networks and Systems, RTNS 2021, pp. 216\u2013225 (2021)","DOI":"10.1145\/3453417.3453437"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/11888116_23","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"L Hillah","year":"2006","unstructured":"Hillah, L., Kordon, F., Petrucci, L., Tr\u00e8ves, N.: PN standardisation: a survey. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 307\u2013322. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11888116_23"},{"key":"9_CR12","unstructured":"ISO: ISO 26262:2018 road vehicles \u2013 functional safety. Technical report, ISO (2018)"},{"key":"9_CR13","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 2009, New York, NY, USA, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"2","key":"9_CR14","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE\u20133","author":"L Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE\u20133(2), 125\u2013143 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-00768-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Lime","year":"2009","unstructured":"Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54\u201357. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_6"},{"key":"9_CR16","unstructured":"OSEK Group: OSEK\/VDX OS test plan version 2.0 (1999)"},{"issue":"4","key":"9_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3015777","volume":"16","author":"KTG Tigori","year":"2017","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. (TECS) 16(4), 1\u201325 (2017)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-17244-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,5]],"date-time":"2024-10-05T12:41:45Z","timestamp":1728132105000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-17244-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031172434","9783031172441"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-17244-1_9","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":"10 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Madrid","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","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":"24 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/maude.ucm.es\/ICFEM22\/index.html","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":"61","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":"23","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":"38% - 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":"3","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)"}},{"value":"3 invited papers (two papers and one abstract)","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}