{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T16:52:44Z","timestamp":1730220764414,"version":"3.28.0"},"reference-count":28,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,9]]},"DOI":"10.1109\/etfa.2017.8247611","type":"proceedings-article","created":{"date-parts":[[2018,1,8]],"date-time":"2018-01-08T22:42:04Z","timestamp":1515451324000},"page":"1-8","source":"Crossref","is-referenced-by-count":5,"title":["Automata-based modeling of interrupts in the Linux PREEMPT RT kernel"],"prefix":"10.1109","author":[{"given":"Daniel B.","family":"de Oliveira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Romulo S.","family":"de Oliveira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tommaso","family":"Cucinotta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Abeni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1137\/0325013"},{"key":"ref11","volume":"3","author":"corporation","year":"2016","journal-title":"Intel 64 and IA-32 Architectures Software Devel-oper's Manual"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2006.382401"},{"key":"ref13","first-page":"483","article-title":"Graph viz-open source graph drawing tools","author":"ellson","year":"2001","journal-title":"International Symposium on Graph Drawing"},{"key":"ref14","first-page":"322","article-title":"An automata-theoretic approach to automatic program verification","author":"vardi","year":"1986","journal-title":"Proc First IEEE Symp Logic in Computer Science"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"ref17","first-page":"36","author":"lamport","year":"2009","journal-title":"The PlusCal Algorithm Language"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186058"},{"key":"ref19","first-page":"206","author":"methni","year":"2015","journal-title":"Specifying and Verifying Concurrent C Programs with TLA +"},{"key":"ref28","article-title":"Realtime Linux: academia v. reality","author":"gleixner","year":"2010","journal-title":"Linux Weekly News"},{"journal-title":"Available at","article-title":"Red Hat Enterprise Linux for Real Time","year":"0","key":"ref4"},{"key":"ref27","first-page":"19","article-title":"Joint Opportunities for Real-Time Linux and Real-Time System Research","author":"brandenbug","year":"2009","journal-title":"Proceedings of the 11th Real-Time Linux Workshop 2009"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1998.739726"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2333"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/RTTAS.2002.1137388"},{"journal-title":"Introduction to Automata Theory Languages and Computations","year":"2006","author":"hopcroft","key":"ref8"},{"key":"ref7","first-page":"105","author":"brandenburg","year":"2008","journal-title":"A comparison of the M-PCP D-PCP and the FMLP on LITMUSRT"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2335"},{"journal-title":"Introduction to Discrete Event Systems","year":"2010","author":"cassandras","key":"ref9"},{"journal-title":"A Realtime Preemption Overview","year":"2005","author":"mckenney","key":"ref1"},{"key":"ref20","first-page":"25","author":"newcombe","year":"2014","journal-title":"Why Amazon Chose TLA +"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"journal-title":"The kernel lock validator","year":"2006","author":"corbet","key":"ref24"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321719"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.38"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"}],"event":{"name":"2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA)","start":{"date-parts":[[2017,9,12]]},"location":"Limassol","end":{"date-parts":[[2017,9,15]]}},"container-title":["2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8233358\/8247555\/08247611.pdf?arnumber=8247611","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,2,12]],"date-time":"2018-02-12T22:53:21Z","timestamp":1518476001000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8247611\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/etfa.2017.8247611","relation":{},"subject":[],"published":{"date-parts":[[2017,9]]}}}