{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T11:44:57Z","timestamp":1790509497454,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,4,7]],"date-time":"2021-04-07T00:00:00Z","timestamp":1617753600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,4,7]]},"DOI":"10.1145\/3453417.3453437","type":"proceedings-article","created":{"date-parts":[[2021,7,22]],"date-time":"2021-07-22T22:18:55Z","timestamp":1626992335000},"page":"216-225","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Formal schedulability analysis based on multi-core RTOS model"],"prefix":"10.1145","author":[{"given":"Imane","family":"Haur","sequence":"first","affiliation":[{"name":"\u00c9cole Centrale de Nantes and Huawei, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Luc","family":"B\u00e9chennec","sequence":"additional","affiliation":[{"name":"CNRS, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Olivier Henri","family":"Roux","sequence":"additional","affiliation":[{"name":"\u00c9cole Centrale de Nantes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,7,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_1_2_1","volume-title":"FTSCS 2018","author":"Andr\u00e9 \u00c9tienne","year":"2018","unstructured":"\u00c9tienne Andr\u00e9 . 2018 . A Benchmark Library for Parametric Timed Model Checking. In Formal Techniques for Safety-Critical Systems - 6th International Workshop , FTSCS 2018 , Gold Coast, Australia , November 16, 2018, Revised Selected Papers(Communications in Computer and Information Science, Vol.\u00a01008), Cyrille Artho and Peter\u00a0Csaba \u00d6lveczky (Eds.). Springer, 75\u201383. https:\/\/doi.org\/10.1007\/978-3-030-12988-0_5 \u00c9tienne Andr\u00e9. 2018. A Benchmark Library for Parametric Timed Model Checking. In Formal Techniques for Safety-Critical Systems - 6th International Workshop, FTSCS 2018, Gold Coast, Australia, November 16, 2018, Revised Selected Papers(Communications in Computer and Information Science, Vol.\u00a01008), Cyrille Artho and Peter\u00a0Csaba \u00d6lveczky (Eds.). Springer, 75\u201383. https:\/\/doi.org\/10.1007\/978-3-030-12988-0_5"},{"key":"e_1_3_2_1_3_1","unstructured":"ARINC Group. 2019. 653P1-5 Avionics Application Software Standard Interface Part 1 Required Services. https:\/\/www.aviation-ia.com\/products\/653p1-5-avionics-application-software-standard-interface-part-1-required-services  ARINC Group. 2019. 653P1-5 Avionics Application Software Standard Interface Part 1 Required Services. https:\/\/www.aviation-ia.com\/products\/653p1-5-avionics-application-software-standard-interface-part-1-required-services"},{"key":"e_1_3_2_1_4_1","unstructured":"AUTOSAR GbR. 2009. Specification of operating system.  AUTOSAR GbR. 2009. Specification of operating system."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_3_2_1_6_1","volume-title":"IEEE Conference on Emerging Technologies and Factory Automation. ETFA\u201906","author":"B\u00e9chennec Jean-Luc","year":"2006","unstructured":"Jean-Luc B\u00e9chennec , Mika\u00ebl Briday , S\u00e9bastien Faucou , and Yvon Trinquet . 2006 . Trampoline an OpenSource Implementation of the OSEK\/VDX RTOS Specification . In IEEE Conference on Emerging Technologies and Factory Automation. ETFA\u201906 . 62\u201369. Jean-Luc B\u00e9chennec, Mika\u00ebl Briday, S\u00e9bastien Faucou, and Yvon Trinquet. 2006. Trampoline an OpenSource Implementation of the OSEK\/VDX RTOS Specification. In IEEE Conference on Emerging Technologies and Factory Automation. ETFA\u201906. 62\u201369."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/CoDIT.2018.8394813"},{"key":"e_1_3_2_1_8_1","volume-title":"Optimal scheduling using priced timed automata. SIGMETRICS Performance Evaluation Review 32 (03","author":"Behrmann Gerd","year":"2005","unstructured":"Gerd Behrmann , Kim Larsen , and Jacob Rasmussen . 2005. Optimal scheduling using priced timed automata. SIGMETRICS Performance Evaluation Review 32 (03 2005 ), 34\u201340. https:\/\/doi.org\/10.1145\/1059816.1059823 Gerd Behrmann, Kim Larsen, and Jacob Rasmussen. 2005. Optimal scheduling using priced timed automata. SIGMETRICS Performance Evaluation Review 32 (03 2005), 34\u201340. https:\/\/doi.org\/10.1145\/1059816.1059823"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.75415"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-006-0011-y"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3394810.3394817"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"G. Bucci A. Fedeli L. Sassoli and E. Vicario. 2004. Time state space analysis of real-time preemptive systems. IEEE transactions on software engineering 30 2 (February 2004) 97\u2013111.  G. Bucci A. Fedeli L. Sassoli and E. Vicario. 2004. Time state space analysis of real-time preemptive systems. IEEE transactions on software engineering 30 2 (February 2004) 97\u2013111.","DOI":"10.1109\/TSE.2004.1265815"},{"key":"e_1_3_2_1_13_1","volume-title":"Safety Analysis of Trampoline OS Using Model Checking: An Experience Report. In 2011 IEEE 22nd International Symposium on Software Reliability Engineering. 200\u2013209","author":"Choi Y.","year":"2011","unstructured":"Y. Choi . 2011 . Safety Analysis of Trampoline OS Using Model Checking: An Experience Report. In 2011 IEEE 22nd International Symposium on Software Reliability Engineering. 200\u2013209 . https:\/\/doi.org\/10.1109\/ISSRE.2011.22 Y. Choi. 2011. Safety Analysis of Trampoline OS Using Model Checking: An Experience Report. In 2011 IEEE 22nd International Symposium on Software Reliability Engineering. 200\u2013209. https:\/\/doi.org\/10.1109\/ISSRE.2011.22"},{"key":"e_1_3_2_1_14_1","volume-title":"TTCS 2015","author":"Dal-Zilio Silvano","year":"2015","unstructured":"Silvano Dal-Zilio and Bernard Berthomieu . 2015 . Automating the Verification of Realtime Observers Using Probes and the Modal mu-calculus. In Topics in Theoretical Computer Science - The First IFIP WG 1.8 International Conference , TTCS 2015 , Tehran, Iran , August 26-28, 2015, Revised Selected Papers(Lecture Notes in Computer Science, Vol.\u00a09541). Springer, 90\u2013104. Silvano Dal-Zilio and Bernard Berthomieu. 2015. Automating the Verification of Realtime Observers Using Probes and the Modal mu-calculus. In Topics in Theoretical Computer Science - The First IFIP WG 1.8 International Conference, TTCS 2015, Tehran, Iran, August 26-28, 2015, Revised Selected Papers(Lecture Notes in Computer Science, Vol.\u00a09541). Springer, 90\u2013104."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1474-6670(17)39938-X"},{"key":"e_1_3_2_1_16_1","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006(Lecture Notes in Computer Science, Vol.\u00a04229)","author":"Hillah Lom","unstructured":"Lom Hillah , F. Kordon , Laure Petrucci , and Nicolas Tr\u00e8ves . 2006. PN Standardisation: A Survey . In Formal Techniques for Networked and Distributed Systems - FORTE 2006(Lecture Notes in Computer Science, Vol.\u00a04229) . Springer Berlin Heidelberg , 307\u2013322. Lom Hillah, F. Kordon, Laure Petrucci, and Nicolas Tr\u00e8ves. 2006. PN Standardisation: A Survey. In Formal Techniques for Networked and Distributed Systems - FORTE 2006(Lecture Notes in Computer Science, Vol.\u00a04229). Springer Berlin Heidelberg, 307\u2013322."},{"key":"e_1_3_2_1_17_1","unstructured":"Michael Hohmuth and H. Tews. 2005. The VFiasco approach for a verified operating system.  Michael Hohmuth and H. Tews. 2005. The VFiasco approach for a verified operating system."},{"key":"e_1_3_2_1_18_1","volume-title":"Modeling and Verifying the Code-Level OSEK\/VDX Operating System with CSP. In 2011 Fifth International Conference on Theoretical Aspects of Software Engineering. 142\u2013149","author":"Huang Y.","year":"2011","unstructured":"Y. Huang , Y. Zhao , L. Zhu , Q. Li , H. Zhu , and J. Shi . 2011 . Modeling and Verifying the Code-Level OSEK\/VDX Operating System with CSP. In 2011 Fifth International Conference on Theoretical Aspects of Software Engineering. 142\u2013149 . https:\/\/doi.org\/10.1109\/TASE. 2011 .11 Y. Huang, Y. Zhao, L. Zhu, Q. Li, H. Zhu, and J. Shi. 2011. Modeling and Verifying the Code-Level OSEK\/VDX Operating System with CSP. In 2011 Fifth International Conference on Theoretical Aspects of Software Engineering. 142\u2013149. https:\/\/doi.org\/10.1109\/TASE.2011.11"},{"key":"e_1_3_2_1_19_1","volume-title":"Proceedings of the Tenth Workshop and Tutorial on Practical Use of Coloured Petri Nets and CPN Tools (CPN \u201909)","author":"Kindler Ekkart","year":"2009","unstructured":"Ekkart Kindler and Laure Petrucci . 2009 . A framework for the definition of variants of high-level Petri nets . In Proceedings of the Tenth Workshop and Tutorial on Practical Use of Coloured Petri Nets and CPN Tools (CPN \u201909) . 121\u2013137. Ekkart Kindler and Laure Petrucci. 2009. A framework for the definition of variants of high-level Petri nets. In Proceedings of the Tenth Workshop and Tutorial on Practical Use of Coloured Petri Nets and CPN Tools (CPN \u201909). 121\u2013137."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_21_1","volume-title":"Formal Verification of Real-time Systems with Preemptive Scheduling. Real-Time Systems 41 (02","author":"Lime Didier","year":"2009","unstructured":"Didier Lime and Olivier Roux . 2009. Formal Verification of Real-time Systems with Preemptive Scheduling. Real-Time Systems 41 (02 2009 ), 118\u2013151. https:\/\/doi.org\/10.1007\/s11241-008-9059-0 Didier Lime and Olivier Roux. 2009. Formal Verification of Real-time Systems with Preemptive Scheduling. Real-Time Systems 41 (02 2009), 118\u2013151. https:\/\/doi.org\/10.1007\/s11241-008-9059-0"},{"key":"e_1_3_2_1_22_1","volume-title":"Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. In 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009)","author":"Lime Didier","year":"2009","unstructured":"Didier Lime , Olivier\u00a0 H. Roux , Charlotte Seidner , and Louis-Marie Traonouez . 2009 . Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. In 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009) (Lecture Notes in Computer Science, Vol.\u00a05505). Springer, 54\u201357. Didier Lime, Olivier\u00a0H. Roux, Charlotte Seidner, and Louis-Marie Traonouez. 2009. Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. In 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009)(Lecture Notes in Computer Science, Vol.\u00a05505). Springer, 54\u201357."},{"key":"e_1_3_2_1_23_1","unstructured":"Thanh\u00a0Dat Nguyen. 2020. Aide \u00e0 la validation temporelle et au dimensionnement de syst\u00e8mes temps r\u00e9els dans une d\u00e9marche dirig\u00e9e par mod\u00e8les. Theses. ISAE-ENSMA Ecole Nationale Sup\u00e9rieure de M\u00e9canique et d\u2019A\u00e9rotechique - Poitiers. https:\/\/tel.archives-ouvertes.fr\/tel-03079085  Thanh\u00a0Dat Nguyen. 2020. Aide \u00e0 la validation temporelle et au dimensionnement de syst\u00e8mes temps r\u00e9els dans une d\u00e9marche dirig\u00e9e par mod\u00e8les. Theses. ISAE-ENSMA Ecole Nationale Sup\u00e9rieure de M\u00e9canique et d\u2019A\u00e9rotechique - Poitiers. https:\/\/tel.archives-ouvertes.fr\/tel-03079085"},{"key":"e_1_3_2_1_24_1","volume-title":"FTSCS 2016","author":"Parquier Baptiste","year":"2016","unstructured":"Baptiste Parquier , Laurent Rioux , Rafik Henia , Romain Soulat , Olivier\u00a0 H. Roux , Didier Lime , and \u00c9tienne Andr\u00e9 . 2016 . Applying Parametric Model-Checking Techniques for Reusing Real-Time Critical Systems. In Formal Techniques for Safety-Critical Systems - 5th International Workshop , FTSCS 2016 , Tokyo, Japan , November 14, 2016, Revised Selected Papers(Communications in Computer and Information Science, Vol.\u00a0694), Cyrille Artho and Peter\u00a0Csaba \u00d6lveczky (Eds.). 129\u2013144. https:\/\/doi.org\/10.1007\/978-3-319-53946-1_8 Baptiste Parquier, Laurent Rioux, Rafik Henia, Romain Soulat, Olivier\u00a0H. Roux, Didier Lime, and \u00c9tienne Andr\u00e9. 2016. Applying Parametric Model-Checking Techniques for Reusing Real-Time Critical Systems. In Formal Techniques for Safety-Critical Systems - 5th International Workshop, FTSCS 2016, Tokyo, Japan, November 14, 2016, Revised Selected Papers(Communications in Computer and Information Science, Vol.\u00a0694), Cyrille Artho and Peter\u00a0Csaba \u00d6lveczky (Eds.). 129\u2013144. https:\/\/doi.org\/10.1007\/978-3-319-53946-1_8"},{"key":"e_1_3_2_1_25_1","unstructured":"Olivier\u00a0H. Roux and Didier Lime. [n.d.]. Rom\u00e9o: formal verification and synthesis for timed systems. http:\/\/romeo.rts-software.org.  Olivier\u00a0H. Roux and Didier Lime. [n.d.]. Rom\u00e9o: formal verification and synthesis for timed systems. http:\/\/romeo.rts-software.org."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:TIME.0000045315.61234.1e"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.57058"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.7053"},{"key":"e_1_3_2_1_29_1","unstructured":"Youcheng Sun Giuseppe Lipari and \u00c9tienne Andr\u00e9. 2015. Verification of Two Real-Time Systems Using Parametric Timed Automata. In WATERS - International Workshop on Analysis Tools and Methodologies for Embedded Real-Time Systems(WATERS - International Workshop on Analysis Tools and Methodologies for Embedded Real-Time Systems). Lund Sweden. https:\/\/hal.archives-ouvertes.fr\/hal-01240583  Youcheng Sun Giuseppe Lipari and \u00c9tienne Andr\u00e9. 2015. Verification of Two Real-Time Systems Using Parametric Timed Automata. In WATERS - International Workshop on Analysis Tools and Methodologies for Embedded Real-Time Systems(WATERS - International Workshop on Analysis Tools and Methodologies for Embedded Real-Time Systems). Lund Sweden. https:\/\/hal.archives-ouvertes.fr\/hal-01240583"},{"key":"e_1_3_2_1_30_1","first-page":"4","article-title":"Formal Model-Based Synthesis of Application-Specific Static RTOS","volume":"16","author":"Toussaint\u00a0Gautier Tigori Kabland","year":"2017","unstructured":"Kabland Toussaint\u00a0Gautier Tigori , Jean-Luc B\u00e9chennec , S\u00e9bastien Faucou , and Olivier\u00a0Henri Roux . 2017 . Formal Model-Based Synthesis of Application-Specific Static RTOS . ACM Transactions on Embedded Computing Systems (TECS) 16 , 4 (Sept. 2017), 1 \u2013 25. https:\/\/doi.org\/10.1145\/3015777 Kabland Toussaint\u00a0Gautier Tigori, Jean-Luc B\u00e9chennec, S\u00e9bastien Faucou, and Olivier\u00a0Henri Roux. 2017. Formal Model-Based Synthesis of Application-Specific Static RTOS. ACM Transactions on Embedded Computing Systems (TECS) 16, 4 (Sept. 2017), 1 \u2013 25. https:\/\/doi.org\/10.1145\/3015777","journal-title":"ACM Transactions on Embedded Computing Systems (TECS)"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-007-9036-z"}],"event":{"name":"RTNS'2021: 29th International Conference on Real-Time Networks and Systems","location":"NANTES France","acronym":"RTNS'2021"},"container-title":["29th International Conference on Real-Time Networks and Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453417.3453437","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453417.3453437","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:03:06Z","timestamp":1750197786000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453417.3453437"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,7]]},"references-count":31,"alternative-id":["10.1145\/3453417.3453437","10.1145\/3453417"],"URL":"https:\/\/doi.org\/10.1145\/3453417.3453437","relation":{},"subject":[],"published":{"date-parts":[[2021,4,7]]},"assertion":[{"value":"2021-07-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}