{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:24:56Z","timestamp":1740122696534,"version":"3.37.3"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2021,1,8]],"date-time":"2021-01-08T00:00:00Z","timestamp":1610064000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,8]],"date-time":"2021-01-08T00:00:00Z","timestamp":1610064000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001501","name":"University Grants Commission","doi-asserted-by":"publisher","award":["F.4-2\/2006 (BSR)\/EN\/17-18\/0039"],"award-info":[{"award-number":["F.4-2\/2006 (BSR)\/EN\/17-18\/0039"]}],"id":[{"id":"10.13039\/501100001501","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Robert Bosch Center for Cyber-Physical Systems"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,10]]},"DOI":"10.1007\/s10703-020-00354-0","type":"journal-article","created":{"date-parts":[[2021,1,8]],"date-time":"2021-01-08T18:03:10Z","timestamp":1610128990000},"page":"294-321","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Static analysis for detecting high-level races in RTOS kernels"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5964-8819","authenticated-orcid":false,"given":"Rekha","family":"Pai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abhishek","family":"Singh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Deepak","family":"D\u2019Souza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meenakshi","family":"D\u2019Souza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Prathibha","family":"Prakash","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,1,8]]},"reference":[{"key":"354_CR1","unstructured":"Ardupilot (2019) https:\/\/ardupilot.org\/"},{"issue":"2","key":"354_CR2","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/1119479.1119480","volume":"28","author":"M Abadi","year":"2006","unstructured":"Abadi M, Flanagan C, Freund SN (2006) Types for safe locking: static race detection for Java. ACM Trans Program Lang Syst TOPLAS 28(2):207\u2013255","journal-title":"ACM Trans Program Lang Syst TOPLAS"},{"issue":"1\u20132","key":"354_CR3","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1999.2847","volume":"160","author":"R Alur","year":"2000","unstructured":"Alur R, McMillan KL, Peled DA (2000) Model-checking of correctness conditions for concurrent objects. Inf Comput 160(1\u20132):167\u2013188","journal-title":"Inf Comput"},{"key":"354_CR4","doi-asserted-by":"crossref","unstructured":"Artho C, Havelund K, Biere A (2003) High-level data races. J Softw Test Verif Reliab 207\u2013227","DOI":"10.1002\/stvr.281"},{"key":"354_CR5","unstructured":"Barry R (2017) The FreeRTOS kernel, v10.0.0. https:\/\/freertos.org"},{"key":"354_CR6","unstructured":"Chopra N, Pai R, D\u2019Souza D (2019) Data races and static analysis for interrupt-driven programs. In: Proceedings of 28th European symposium on programming (ESOP), Prague, Czech Republic. LNCS, vol 11423, pp 1\u201327. Springer"},{"key":"354_CR7","unstructured":"Di\u00a0Sirio G (2019) ChibiOS kernel, v19.1.0. http:\/\/www.chibios.org\/dokuwiki\/doku.php"},{"key":"354_CR8","doi-asserted-by":"crossref","unstructured":"Dias RJ, Pessanha V, Louren\u00e7o J (2012) Precise detection of atomicity violations. In: Hardware and software: verification and testing\u20148th international Haifa verification conference (HVC), pp 8\u201323","DOI":"10.1007\/978-3-642-39611-3_8"},{"key":"354_CR9","unstructured":"Elmas T, Qadeer S, Tasiran S (2005) Precise race detection and efficient model checking using locksets. Tech. Rep. MSR-TR-2005-118, Microsoft Research"},{"issue":"5","key":"354_CR10","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/1165389.945468","volume":"37","author":"D Engler","year":"2003","unstructured":"Engler D, Ashcraft K (2003) Racerx: effective, static detection of race conditions and deadlocks. SIGOPS Oper Syst Rev 37(5):237\u2013252","journal-title":"SIGOPS Oper Syst Rev"},{"key":"354_CR11","doi-asserted-by":"crossref","unstructured":"Flanagan C, Qadeer S (2003) A type and effect system for atomicity. In: Proceedings of ACM SIGPLAN programming language design and implementation (PLDI), pp 338\u2013349","DOI":"10.1145\/780822.781169"},{"issue":"8","key":"354_CR12","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1109\/32.940728","volume":"27","author":"K Havelund","year":"2001","unstructured":"Havelund K, Lowry MR, Penix J (2001) Formal analysis of a space-craft controller using SPIN. IEEE Trans Softw Eng 27(8):749\u2013765","journal-title":"IEEE Trans Softw Eng"},{"key":"354_CR13","doi-asserted-by":"crossref","unstructured":"Havelund K, Skakkeb\u00e6k JU (1999) Applying model checking in java verification. In: Proceedings of theoretical and practical aspects of SPIN model checking, vol 1680, pp 216\u2013231. Springer","DOI":"10.1007\/3-540-48234-2_17"},{"key":"354_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R (2004) Race checking by context inference. In: Proceedings of ACM SIGPLAN programming language design and implementation (PLDI), pp 1\u201313","DOI":"10.1145\/996893.996844"},{"key":"354_CR15","unstructured":"Instruments T (2017) TI-RTOS: a real-time operating system for microcontrollers. http:\/\/www.ti.com\/tool\/ti-rtos"},{"key":"354_CR16","doi-asserted-by":"crossref","unstructured":"Mukherjee S, Kumar A, D\u2019Souza D (2017) Detecting all high-level data races in an RTOS kernel. In: Proceedings of verification, model checking, and abstract interpretation (VMCAI), proceedings, pp 405\u2013423","DOI":"10.1007\/978-3-319-52234-0_22"},{"key":"354_CR17","unstructured":"Necula G (2002) CIL\u2014infrastructure for C program analysis and transformation (v. 1.3.7). http:\/\/people.eecs.berkeley.edu\/~necula\/cil\/"},{"issue":"9","key":"354_CR18","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.entcs.2007.04.002","volume":"174","author":"J Regehr","year":"2007","unstructured":"Regehr J, Cooprider N (2007) Interrupt verification via thread verification. Electr Notes Theor Comput Sci 174(9):139\u2013150","journal-title":"Electr Notes Theor Comput Sci"},{"issue":"4","key":"354_CR19","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S Savage","year":"1997","unstructured":"Savage S, Burrows M, Nelson G, Sobalvarro P, Anderson TE (1997) Eraser: a dynamic data race detector for multi-threaded programs. ACM Trans Comput Syst 15(4):391\u2013411","journal-title":"ACM Trans Comput Syst"},{"key":"354_CR20","doi-asserted-by":"crossref","unstructured":"Schwarz MD, Seidl H, Vojdani V, Apinis K (2014) Precise analysis of value-dependent synchronization in priority scheduled programs. In: Proceedings of verification, model checking, and abstract interpretation (VMCAI), pp 21\u201338","DOI":"10.1007\/978-3-642-54013-4_2"},{"key":"354_CR21","doi-asserted-by":"crossref","unstructured":"Schwarz MD, Seidl H, Vojdani V, Lammich P, M\u00fcller-Olm M (2011) Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. In: Proceedings of ACM SIGPLAN-SIGACT principles of programming languages (POPL), pp 93\u2013104","DOI":"10.1145\/1925844.1926398"},{"key":"354_CR22","doi-asserted-by":"crossref","unstructured":"Singh A, Pai R, D\u2019Souza D, D\u2019Souza M (2019) Static analysis for detecting high-level races in RTOS kernels. In: Formal methods\u2014the next 30 years\u2014third world congress (FM), Porto, proceedings, pp 337\u2013353","DOI":"10.1007\/978-3-030-30942-8_21"},{"key":"354_CR23","unstructured":"Sterling N (1993) WARLOCK\u2014a static data race analysis tool. In: Proc. Usenix winter technical conference, pp 97\u2013106"},{"key":"354_CR24","doi-asserted-by":"crossref","unstructured":"Sung C, Kusano M, Wang C (2017) Modular verification of interrupt-driven software. In: Proceedings of the 32nd IEEE\/ACM international conference on automated software engineering (ASE), pp 206\u2013216","DOI":"10.1109\/ASE.2017.8115634"},{"issue":"6","key":"354_CR25","doi-asserted-by":"publisher","first-page":"103","DOI":"10.5381\/jot.2004.3.6.a5","volume":"3","author":"C von Praun","year":"2004","unstructured":"von Praun C, Gross TR (2004) Static detection of atomicity violations in object-oriented programs. J Object Technol 3(6):103\u2013122","journal-title":"J Object Technol"},{"key":"354_CR26","doi-asserted-by":"crossref","unstructured":"Voung JW, Jhala R, Lerner S (2007) RELAY: static race detection on millions of lines of code. In: Proceedings of ESEC\/SIGSOFT foundation software engineering (FSE), pp 205\u2013214","DOI":"10.1145\/1287624.1287654"},{"key":"354_CR27","doi-asserted-by":"crossref","unstructured":"Wang Y, Wang L, Yu T, Zhao J, Li X (2017) Automatic detection and validation of race conditions in interrupt-driven embedded software. In: Proceedings of the 26th ACM SIGSOFT international symposium on software testing and analysis (ISSTA). ACM, pp 113\u2013124","DOI":"10.1145\/3092703.3092724"},{"key":"354_CR28","doi-asserted-by":"crossref","unstructured":"Zeng R, Sun Z, Liu S, He X (2012) Mcpatom: a predictive analysis tool for atomicity violation using model checking. In: Proceedings of model checking software (SPIN), pp 191\u2013207","DOI":"10.1007\/978-3-642-31759-0_14"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00354-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-020-00354-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00354-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,26]],"date-time":"2022-08-26T15:50:39Z","timestamp":1661529039000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-020-00354-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,8]]},"references-count":28,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["354"],"URL":"https:\/\/doi.org\/10.1007\/s10703-020-00354-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2021,1,8]]},"assertion":[{"value":"2 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 November 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 January 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}