{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T15:24:58Z","timestamp":1759937098496,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308253"},{"type":"electronic","value":"9783031308260"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The use of formal methods to prove the correctness of compositional embedded systems is increasingly important. However, the required models and algorithms can induce an enormous complexity. Our approach divides the formal system model into layers and these in turn into modules with defined interfaces, so that reduced formal models can be created for the verification of concrete functional and non-functional requirements. In this work, we use <jats:sc>Uppaal<\/jats:sc> to (1) model an RTOS kernel in a modular way and formally specify its internal requirements, (2) model abstract tasks that trigger all kernel functionalities in all combinations or scenarios, and (3) verify the resulting system with regard to task synchronization, resource management, and timing. The result is a fully verified model of the operating system layer that can henceforth serve as a dependable foundation for verifying compositional applications w.r.t. various aspects, such as timing or liveness.<\/jats:p>","DOI":"10.1007\/978-3-031-30826-0_2","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T18:02:59Z","timestamp":1681927379000},"page":"26-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Modeling Concept for Formal Verification of OS-Based Compositional Software"],"prefix":"10.1007","author":[{"given":"Leandro Batista","family":"Ribeiro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Lorber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ulrik","family":"Nyman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcel","family":"Baunach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"2_CR1","unstructured":"FreeRTOS. https:\/\/freertos.org\/. [Online; accessed 20-January-2023]."},{"key":"2_CR2","unstructured":"The Coq proof assistant. https:\/\/coq.inria.fr\/. [Online; accessed 20-January-2023]."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Jean-Raymond Abrial. Modeling in Event-B: system and software engineering. Cambridge University Press, 2010.","DOI":"10.1017\/CBO9781139195881"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Benny Akesson, Mitra Nasri, Geoffrey Nelissen, Sebastian Altmeyer, and Robert\u00a0I Davis. A comprehensive survey of industry practice in real-time systems. Real-Time Systems, 2021.","DOI":"10.1109\/RTSS49844.2020.00012"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Eman\u00a0H Alkhammash et\u00a0al. Modeling guidelines of FreeRTOS in Event-B. In Shaping the Future of ICT. CRC Press, 2017.","DOI":"10.1201\/9781315155241-15"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Mike Barnett, Bor-Yuh\u00a0Evan Chang, Robert DeLine, Bart Jacobs, and K.\u00a0Rustan\u00a0M. Leino. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg.","DOI":"10.1007\/11804192_17"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Gerd Behrmann, Alexandre David, and Kim\u00a0G Larsen. A tutorial on Uppaal. Formal methods for the design of real-time systems, 2004.","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Aimee Borda, Liliana Pasquale, Vasileios Koutavas, and Bashar Nuseibeh. Compositional Verification of Self-Adaptive Cyber-Physical Systems. In 2018 IEEE\/ACM 13th Int\u2019l Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), 2018.","DOI":"10.1145\/3194133.3194146"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Robert Brummayer and Armin Biere. Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In Tools and Algorithms for the Construction and Analysis of Systems, Berlin, Heidelberg, 2009.","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Franck Cassez and Kim Larsen. The impressive power of stopwatches. In International Conference on Concurrency Theory. Springer, 2000.","DOI":"10.1007\/3-540-44618-4_12"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Shu Cheng, Jim Woodcock, and Deepak D\u2019Souza. Using formal reasoning on a model of tasks for FreeRTOS. Formal Aspects of Computing, 27(1), 2015.","DOI":"10.1007\/s00165-014-0308-9"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Holger Giese et\u00a0al. Towards the Compositional Verification of Real-Time UML Designs. In 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT Int\u2019l Symposium on Foundations of Software Engineering, New York, NY, USA, 2003.","DOI":"10.1145\/940071.940078"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Mario Gleirscher, Simon Foster, and Jim Woodcock. New Opportunities for Integrated Formal Methods. ACM Comput. Surv., 52(6), oct 2019.","DOI":"10.1145\/3357231"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Tom\u00e1s Grimm, Djones Lettnin, and Michael H\u00fcbner. A Survey on Formal Verification Techniques for Safety-Critical Systems-on-Chip. Electronics, 7(6), 2018.","DOI":"10.3390\/electronics7060081"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Ronghui Gu et\u00a0al. Deep Specifications and Certified Abstraction Layers. ACM SIGPLAN Notices, 50(1), jan 2015.","DOI":"10.1145\/2775051.2676975"},{"key":"2_CR16","unstructured":"Ronghui Gu et\u00a0al. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), Savannah, GA, November 2016. USENIX Association."},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Pujie Han, Zhengjun Zhai, Brian Nielsen, and Ulrik Nyman. A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems. In 1st Int\u2019l Workshop on Methods and Tools for Rigorous System Design (MeTRiD@ETAPS), Greece, EPTCS, 2018.","DOI":"10.4204\/EPTCS.272.4"},{"key":"2_CR18","unstructured":"Chris Hawblitzel et\u00a0al. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14), Broomfield, CO, October 2014. USENIX Association."},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Joseph Herkert, Jason Borenstein, and Keith Miller. The Boeing 737 MAX: Lessons for engineering ethics. Science and engineering ethics, 26(6), 2020.","DOI":"10.1007\/s11948-020-00252-y"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Gerwin Klein et\u00a0al. SeL4: Formal Verification of an OS Kernel. In ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP \u201909, New York, NY, USA, 2009.","DOI":"10.1145\/1629575.1629596"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"John\u00a0C. Knight. Safety Critical Systems: Challenges and Directions. In 24th Int\u2019l Conference on Software Engineering, ICSE \u201902, New York, NY, USA, 2002.","DOI":"10.1145\/581339.581406"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Kim\u00a0G. Larsen, Marius Miku\u010dionis, Marco Mu\u00f1iz, and Ji\u0159\u00ed Srba. Urgent partial order reduction for extended timed automata. In Dang\u00a0Van Hung and Oleg Sokolsky, editors, Automated Technology for Verification and Analysis, pages 179\u2013195, Cham, 2020. Springer International Publishing.","DOI":"10.1007\/978-3-030-59152-6_10"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Kim\u00a0G Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a nutshell. Int\u2019l journal on software tools for technology transfer, 1997.","DOI":"10.1007\/s100090050010"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Thierry Lecomte et\u00a0al. Applying a Formal Method in Industry: A 25-Year Trajectory. In Formal Methods: Foundations and Applications, Cham, 2017. Springer International Publishing.","DOI":"10.1007\/978-3-319-70848-5_6"},{"key":"2_CR25","unstructured":"K.\u00a0Rustan\u00a0M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg."},{"key":"2_CR26","unstructured":"Irwin Meisels and Mark Saaltink. The Z\/EVES reference manual (for version 1.5). Reference manual, ORA Canada, 1997."},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Luke Nelson et\u00a0al. Hyperkernel: Push-Button Verification of an OS Kernel. In 26th Symposium on Operating Systems Principles, SOSP \u201917, New York, NY, USA, 2017. Association for Computing Machinery.","DOI":"10.1145\/3132747.3132748"},{"key":"2_CR28","unstructured":"Tobias Scheipel, Leandro Batista\u00a0Ribeiro, Tim Sagaster, and Marcel Baunach. SmartOS: An OS Architecture for Sustainable Embedded Systems. In Tagungsband des FG-BS Fr\u00fchjahrstreffens 2022, Bonn, 2022. Gesellschaft f\u00fcr Informatik e.V."},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Abhishek Singh, Meenakshi D\u2019Souza, and Arshad Ebrahim. Conformance Testing of ARINC 653 Compliance for a Safety Critical RTOS Using UPPAAL Model Checker. New York, NY, USA, 2021.","DOI":"10.1145\/3412841.3442053"},{"key":"2_CR30","unstructured":"UNECE. UN Regulation No. 156 \u2013 Uniform provisions concerning the approval of vehicles with regards to software update and software updates management system. [online] https:\/\/unece.org\/sites\/default\/files\/2021-03\/R156e.pdf."},{"key":"2_CR31","unstructured":"Virginie WIELS et\u00a0al. Formal Verification of Critical Aerospace Software. Aerospace Lab, May 2012."},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Jianzhou Zhao et\u00a0al. Formalizing the LLVM Intermediate Representation for Verified Program Transformations. In 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201912, New York, NY, USA, 2012. Association for Computing Machinery.","DOI":"10.1145\/2103656.2103709"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30826-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,22]],"date-time":"2023-05-22T22:02:16Z","timestamp":1684792936000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30826-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308253","9783031308260"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30826-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/fase","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":"50","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":"12","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":"24% - 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":"6-7","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":"The proceedings also include 2 tool papers, 2 NIER papers, and 2 competition papers","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)"}}]}}