{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T23:49:55Z","timestamp":1725752995830},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642412011"},{"type":"electronic","value":"9783642412028"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41202-8_12","type":"book-chapter","created":{"date-parts":[[2013,10,21]],"date-time":"2013-10-21T01:11:19Z","timestamp":1382317879000},"page":"165-181","source":"Crossref","is-referenced-by-count":2,"title":["Deadline Analysis of AUTOSAR OS Periodic Tasks in the Presence of Interrupts"],"prefix":"10.1007","author":[{"given":"Yanhong","family":"Huang","sequence":"first","affiliation":[]},{"given":"Jo\u00e3o F.","family":"Ferreira","sequence":"additional","affiliation":[]},{"given":"Guanhua","family":"He","sequence":"additional","affiliation":[]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"AUTOSAR. Specification of Operating System V3.1.1 R3.1 Rev 0002 (2012), http:\/\/www.autosar.org\/ (last accessed: July 1, 2013)"},{"key":"12_CR2","unstructured":"OSEK\/VDX, http:\/\/www.osek-vdx.org\/ (last accessed: July 1, 2013)"},{"key":"12_CR3","unstructured":"Arctic Core \u2014 the open-source AUTOSAR embedded platform, http:\/\/www.arccore.com\/ (last accessed: July 1, 2013)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenstr\u00f6m, P.: The worst-case execution-time problem\u2014overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst.\u00a07(3) (2008)","DOI":"10.1145\/1347375.1347389"},{"key":"12_CR5","unstructured":"Tuch, H.: Formal Memory Models for Verifying C Systems Code. Ph.D. Thesis. University of NSW, Australia (2008)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Regehr, J., Reid, A., Webb, K.: Eliminating stack overflow by abstract interpretation. In: EMSOFT (2003)","DOI":"10.1007\/978-3-540-45212-6_20"},{"key":"12_CR7","unstructured":"Leyva-del-Foyo, L.E., Mejia-Alvarez, P., de Niz, D.: Predictable Interrupt Management for Real Time Kernels over conventional PC Hardware. In: RTAS (2006)"},{"key":"12_CR8","unstructured":"Wolfram Research, Inc., Mathematica, Version 8.0, Champaign, IL (2010)."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Bertrand, D., Faucou, S., Trinquet, Y.: An analysis of the AUTOSAR OS timing protection mechanism. In: ETFA (2009)","DOI":"10.1109\/ETFA.2009.5347159"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Hladik, P.E., Deplanche, A.M., Faucou, S., Trinquet, Y.: Adequacy between AUTOSAR OS specification and real-time scheduling theory. In: SIES (2007)","DOI":"10.1109\/SIES.2007.4297339"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Liu, C.L., Layland, J.W.: Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment. Jounal of the Assocaition for Computing Macheinery\u00a020(1) (1973)","DOI":"10.1145\/321738.321743"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Lehoczky, J.P.: Fixed priority scheduling of periodic task sets with arbitrary deadlines. In: RTSS (1990)","DOI":"10.1109\/REAL.1990.128748"},{"key":"12_CR13","unstructured":"Harbour, M.G., Klein, M.H., Lehoczky, J.P.: Fixed Priority Scheduling of Periodic Tasks with Varying Execution Priority. In: RTSS (1991)"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Katcher, D.I., Arakawa, H., Strosnider, J.K.: Engineering and analysis of fixed priority schedulers. IEEE Transactions on Software Engineering (1993)","DOI":"10.1109\/32.241774"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-540-40903-8_6","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T. Amnell","year":"2004","unstructured":"Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Wang, Y.: TIMES: a Tool for Schedulability Analysis and Code Generation of Real-Time Systems. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.\u00a02791, pp. 60\u201372. Springer, Heidelberg (2004)"},{"key":"12_CR16","unstructured":"Fersman, E., Wang, Y.: A Generic Approach to Schedulability Analysis of Real Time Tasks. Nordic Journal of Computing\u00a011(2) (2004)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-540-24730-2_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Krcal","year":"2004","unstructured":"Krcal, P., Wang, Y.: Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 236\u2013250. Springer, Heidelberg (2004)"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Fersman, E., Mokrushin, L., Pettersson, P., Wang, Y.: Schedulability Analysis of Fixed-Priority Systems Using Timed Automata. Journal of Theoretical Computer Science\u00a0354(2) (2006)","DOI":"10.1016\/j.tcs.2005.11.019"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Brylow, D., Palsberg, J.: Deadline Analysis of Interrupt-Driven Software. IEEE Transactions on Software Engineering (2004)","DOI":"10.1109\/TSE.2004.64"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Schwarz, M.D., Seidl, H., Vojdani, V., Lammich, P., Muller-Olm, M.: Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. In: POPL (2011)","DOI":"10.1145\/1926385.1926398"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. J. Autom. Reasoning\u00a042(2-4) (2009)","DOI":"10.1007\/s10817-009-9118-9"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Zhao, Y., Huang, Y., He, J., Liu, S.: Formal Model of Interrupt Program from a Probabilistic Perspective. In: ICECCS (2011)","DOI":"10.1109\/ICECCS.2011.16"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Shi, J., Zhu, H., He, J., Fang, H., Huang, Y., Zhang, X.: ORIENTAIS: Formal Verified OSEK\/VDX Real-Time Operating System. In: ICECCS (2012)","DOI":"10.1109\/ICECCS20050.2012.6299224"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41202-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,6]],"date-time":"2020-08-06T03:10:02Z","timestamp":1596683402000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41202-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642412011","9783642412028"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41202-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}