{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:50:42Z","timestamp":1740124242013,"version":"3.37.3"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2023,5,25]],"date-time":"2023-05-25T00:00:00Z","timestamp":1684972800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,5,25]],"date-time":"2023-05-25T00:00:00Z","timestamp":1684972800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100003816","name":"Huawei Technologies","doi-asserted-by":"publisher","award":["CIFRE2019-0798"],"award-info":[{"award-number":["CIFRE2019-0798"]}],"id":[{"id":"10.13039\/501100003816","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["CIFRE2019-0798"],"award-info":[{"award-number":["CIFRE2019-0798"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Software Qual J"],"published-print":{"date-parts":[[2023,6]]},"DOI":"10.1007\/s11219-023-09626-4","type":"journal-article","created":{"date-parts":[[2023,5,25]],"date-time":"2023-05-25T10:02:31Z","timestamp":1685008951000},"page":"497-531","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal verification process of the compliance of a multicore AUTOSAR OS"],"prefix":"10.1007","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7569-8587","authenticated-orcid":false,"given":"Imane","family":"Haur","sequence":"first","affiliation":[]},{"given":"Jean-Luc","family":"B\u00e9chennec","sequence":"additional","affiliation":[]},{"given":"Olivier","family":"H. Roux","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,5,25]]},"reference":[{"key":"9626_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., & Dill, D. (1993). Model-checking in dense real-time. Information and Computation, 104, 2\u201334.","journal-title":"Information and Computation"},{"key":"9626_CR2","unstructured":"AUTOSAR. (2010, November). AUTOSAR BSW and RTE Conformance Test Specification Part 2: Process Overview\u00a0(Technical Report). AUTOSAR Consortium."},{"key":"9626_CR3","unstructured":"AUTOSAR GbR. (2009). Specification of operating system."},{"key":"9626_CR4","unstructured":"AUTOSAR. (2014,\u00a0March). Specification of operating system (Technical Report ). AUTOSAR Consortium."},{"key":"9626_CR5","doi-asserted-by":"crossref","unstructured":"B\u00e9chennec, J.-L., Roux, O. H., & Tigori, T. (2018, April). Formal model-based conformance verification of an OSEK\/VDX compliant RTOS. In International Conference on Control, Decision and Information Technologies (CODIT 2018).","DOI":"10.1109\/CoDIT.2018.8394813"},{"key":"9626_CR6","doi-asserted-by":"publisher","first-page":"1509","DOI":"10.1093\/logcom\/exp036","volume":"19","author":"H Boucheneb","year":"2009","unstructured":"Boucheneb, H., Gardey, G., & Roux, O. H. (2009). TCTL model checking of time Petri nets. Journal of Logic and Computation, 19, 1509\u20131540.","journal-title":"Journal of Logic and Computation"},{"key":"9626_CR7","doi-asserted-by":"crossref","unstructured":"Boukir, K., B\u00e9chennec, J.-L., & D\u00e9planche, A.-M. (2020). Requirement specification and model-checking of a real-time scheduler implementation. In Proceedings of the 28th International Conference on Real-Time Networks and Systems RTNS 2020 (pp. 89\u201399). New York, NY, USA: Association for Computing Machinery.","DOI":"10.1145\/3394810.3394817"},{"key":"9626_CR8","doi-asserted-by":"crossref","unstructured":"Boyer, M., & Diaz, M. (2001). Multiple enabledness of transitions in Petri nets with time. In Proceedings of the 9th International Workshop on Petri Nets and Performance Models, PNPM 2001, Aachen, Germany, September 11-14, 2001 (pp. 219\u2013228). IEEE Computer Society.","DOI":"10.1109\/PNPM.2001.953371"},{"key":"9626_CR9","doi-asserted-by":"crossref","unstructured":"Chen, J., & Aoki, T. (2011). Conformance testing for OSEK\/VDX operating system using model checking. In Software Engineering Conference (APSEC), 18th Asia Pacific (pp. 274\u2013281).","DOI":"10.1109\/APSEC.2011.26"},{"key":"9626_CR10","doi-asserted-by":"crossref","unstructured":"Choi, Y. (2011). Safety analysis of Trampoline OS using model checking: An experience report. In 2011 IEEE 22nd International Symposium on Software Reliability Engineering (pp. 200\u2013209).","DOI":"10.1109\/ISSRE.2011.22"},{"key":"9626_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Filkorn, T., & Jha, S. (1993). Exploiting symmetry in temporal logic model checking. In Proceedings of the 5th International Conference on Computer Aided Verification CAV \u201993 (pp. 450\u2013462). Berlin, Heidelberg: Springer-Verlag.","DOI":"10.1007\/3-540-56922-7_37"},{"key":"9626_CR12","doi-asserted-by":"crossref","unstructured":"Cook, S. A. (1971). The complexity of theorem-proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing STOC \u201971 (pp. 151\u2013158). New York, NY, USA: Association for Computing Machinery.","DOI":"10.1145\/800157.805047"},{"key":"9626_CR13","doi-asserted-by":"crossref","unstructured":"Fang, L., Kitamura, T., Do, T. B. N., & Ohsaki, H. (2012). Formal model-based test for AUTOSAR multicore RTOS. In 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation (pp. 251\u2013259).","DOI":"10.1109\/ICST.2012.105"},{"key":"9626_CR14","doi-asserted-by":"crossref","unstructured":"Gadelha, M. R., Monteiro, F. R., Morse, J., Cordeiro, L. C., Fischer, B., & Nicole, D. A. (2018). ESBMC 5.0: An industrial-strength C model checker. In Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering (pp. 888\u2013891). New York, NY, USA: Association for Computing Machinery.","DOI":"10.1145\/3238147.3240481"},{"key":"9626_CR15","unstructured":"Group, O. et al. (2005). OSEK\/VDK operating system specification. http:\/\/www.osek-vdx.org"},{"key":"9626_CR16","doi-asserted-by":"crossref","unstructured":"Haur, I., B\u00e9chennec, J.-L., & Roux, O. H. (2021). Formal schedulability analysis based on multi-core RTOS model. In\u00a029th International Conference on Real-Time Networks and Systems RTNS\u20192021 (pp. 216\u2013225). Association for Computing Machinery: New York, NY, USA.","DOI":"10.1145\/3453417.3453437"},{"key":"9626_CR17","doi-asserted-by":"crossref","unstructured":"Haur, I., B\u00e9chennec, J., & Roux, O. H. (2022a). High-level Colored Time Petri Nets for true concurrency modeling in real-time software. In 8th International Conference on Control, Decision and Information Technologies, CoDIT 2022, Istanbul, Turkey, May 17-20, 2022 (pp. 21\u201326). IEEE.","DOI":"10.1109\/CoDIT55151.2022.9803922"},{"key":"9626_CR18","doi-asserted-by":"crossref","unstructured":"Haur, I., B\u00e9chennec, J., & Roux, O. H. (2022b). 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). Istanbul, Turkey.","DOI":"10.1109\/CoDIT55151.2022.9803922"},{"key":"9626_CR19","doi-asserted-by":"crossref","unstructured":"Hillah, L., Kordon, F., Petrucci, L., & Tr\u00e8ves, N. (2006). Pn standardisation: A survey. In Formal Techniques for Networked and Distributed Systems - FORTE 2006 (pp. 307\u2013322). volume 4229 of Lecture Notes in Computer Science. Springer.","DOI":"10.1007\/11888116_23"},{"key":"9626_CR20","doi-asserted-by":"crossref","unstructured":"Huang, Y., Zhao, Y., Zhu, L., Li, Q., Zhu, H., & Shi, J. (2011). Modeling and verifying the code-level OSEK\/VDK operating system with CSP. In 2011 Fifth International Conference on Theoretical Aspects of Software Engineering (pp. 142\u2013149). IEEE.","DOI":"10.1109\/TASE.2011.11"},{"key":"9626_CR21","doi-asserted-by":"crossref","unstructured":"John, D. (1998). OSEK\/VDX conformance testing - MODISTARC. IET Conference Proceedings, (pp. 7\u20137(1)).","DOI":"10.1049\/ic:19981078"},{"key":"9626_CR22","unstructured":"Kindler, E., & Petrucci, L. (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) (pp. 121\u2013137)."},{"key":"9626_CR23","doi-asserted-by":"crossref","unstructured":"Lime, D., Roux, O. H., Seidner, C., & Traonouez, L.-M. (2009). Romeo: A parametric model-checker for Petri nets with stopwatches. In S. Kowalewski, & A. Philippou (Eds.), 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009) (pp. 54\u201357). York, United Kingdom: Springer volume 5505 of Lecture Notes in Computer Science.","DOI":"10.1007\/978-3-642-00768-2_6"},{"key":"9626_CR24","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T. (1989). Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77, 541\u2013580.","journal-title":"Proceedings of the IEEE"},{"key":"9626_CR25","unstructured":"OSEK Group (1999). OSEK\/VDX OS test plan version 2.0."},{"key":"9626_CR26","doi-asserted-by":"crossref","unstructured":"Peng, Y., Huang, Y., Su, T., & Guo, J. (2013). Modeling and verification of AUTOSAR OS and EMS application. In 2013 International Symposium on Theoretical Aspects of Software Engineering (pp. 37\u201344).","DOI":"10.1109\/TASE.2013.13"},{"key":"9626_CR27","unstructured":"Roux, O. H., & Lime,\u00a0D. (2000). Rom\u00e9o: formal verification and synthesis for parametric timed systems. http:\/\/romeo.rts-software.org\/?page_id=3."},{"key":"9626_CR28","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. (2017). Formal model-based synthesis of application-specific static RTOS. ACM Transactions on Embedded Computing Systems (TECS), 16, 1\u201325.","journal-title":"ACM Transactions on Embedded Computing Systems (TECS)"},{"key":"9626_CR29","doi-asserted-by":"crossref","unstructured":"Trinh, L. K., Chiba, Y., & Aoki, T. (2018). Formalization and verification of AUTOSAR OS standard\u2019s memory protection. In 2018 International Symposium on Theoretical Aspects of Software Engineering (TASE) (pp. 68\u201375).","DOI":"10.1109\/TASE.2018.00017"},{"key":"9626_CR30","doi-asserted-by":"crossref","unstructured":"Yan, R., & Guo, J. (2019). Timing modeling and analysis for AUTOSAR schedule tables. In 2019 IEEE 19th International Symposium on High Assurance Systems Engineering (HASE) (pp. 123\u2013130).","DOI":"10.1109\/HASE.2019.00027"}],"container-title":["Software Quality Journal"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-023-09626-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11219-023-09626-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-023-09626-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,30]],"date-time":"2023-06-30T10:23:12Z","timestamp":1688120592000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11219-023-09626-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,25]]},"references-count":30,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,6]]}},"alternative-id":["9626"],"URL":"https:\/\/doi.org\/10.1007\/s11219-023-09626-4","relation":{},"ISSN":["0963-9314","1573-1367"],"issn-type":[{"type":"print","value":"0963-9314"},{"type":"electronic","value":"1573-1367"}],"subject":[],"published":{"date-parts":[[2023,5,25]]},"assertion":[{"value":"14 March 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 May 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}