{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T16:13:27Z","timestamp":1761581607397,"version":"3.41.0"},"reference-count":13,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"10","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2017]]},"DOI":"10.1587\/transinf.2017edl8090","type":"journal-article","created":{"date-parts":[[2017,9,30]],"date-time":"2017-09-30T22:24:41Z","timestamp":1506810281000},"page":"2644-2647","source":"Crossref","is-referenced-by-count":2,"title":["Timed Model-Based Formal Analysis of a Scheduler of Qplus-AIR, an ARINC-653 Compliance RTOS"],"prefix":"10.1587","volume":"E100.D","author":[{"given":"Sanghyun","family":"YOON","sequence":"first","affiliation":[{"name":"Division of Computer Science and Engineering, Konkuk University"}]},{"given":"Dong-Ah","family":"LEE","sequence":"additional","affiliation":[{"name":"Division of Computer Science and Engineering, Konkuk University"}]},{"given":"Eunji","family":"PAK","sequence":"additional","affiliation":[{"name":"Dependable Software Lab., SW\u00b7Contents Research Division, Electronics and Telecommunications Research Institute"}]},{"given":"Taeho","family":"KIM","sequence":"additional","affiliation":[{"name":"Dependable Software Lab., SW\u00b7Contents Research Division, Electronics and Telecommunications Research Institute"}]},{"given":"Junbeom","family":"YOO","sequence":"additional","affiliation":[{"name":"Division of Computer Science and Engineering, Konkuk University"}]}],"member":"532","reference":[{"key":"1","unstructured":"[1] I. IEC, \u201c61508 functional safety of electrical\/electronic\/prog-rammable electronic safety-related systems,\u201d International electrotechnical commission, 1998. 10.3403\/03263848"},{"key":"2","unstructured":"[2] Radio Technical Commission for Aeronautics (RTCA), \u201cDO-178C: Software Considerations in Airborne Software,\u201d 2011."},{"key":"3","unstructured":"[3] T. Kim, D. Son, C. Shin, S. Park, D. Lim, H. Lee, B. Gim, and C. Lim, \u201cQplus-air: A do-178b certifiable arinc 653 rtos,\u201d The 8th International Symposium on Embedded Technology (ISET), 2013."},{"key":"4","unstructured":"[4] D. Choi, S. Jang, J. Kim, C. Ryu, I. Cho, and T. Kim, \u201cA study on development of UAV flight control software using Qplus-AIR,\u201d The 2012 Spring Conference of the Korean Society for Aeronautical & Space Sciences, pp.1176-1180, The Korean Society For Aeronautical And Space Sciences, 2012."},{"key":"5","unstructured":"[5] T. Kim, D. Son, C. Shin, S. Park, D. Lim, H. Lee, B. Gim, and C. Lim, \u201cQplus\/Esto-AIR: DO-178B Level A Certified RTOS and IDE for Supporting ARINC 653,\u201d Communications of the Korean Institute of Information Scientists and Engineers, vol.30, pp.65-70, 2012."},{"key":"6","unstructured":"[6] T. Kim, D. Son, C. Shin, S. Park, D. Lim, H. Lee, and B. Gim, \u201cExperience of DO-178B Certification of Qplus-AIR,\u201d Communications of the Korean Institute of Information Scientists and Engineers, vol.31, pp.32-39, 2013."},{"key":"7","unstructured":"[7] Airlines Electronic Engineering Committee, \u201cAvionics application software standard interface part 1-Required Service,\u201d ARINC Document ARINC Specification 653P1-2, Aeronautical Radio, Annapolis, Maryland, 2006."},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] B. Dutertre, \u201cFormal analysis of the priority ceiling protocol,\u201d Proc. 21st IEEE Real-Time Systems Symposium, pp.151-160, IEEE, 2000. 10.1109\/real.2000.896005","DOI":"10.1109\/REAL.2000.896005"},{"key":"9","doi-asserted-by":"crossref","unstructured":"[9] T. Amnell, E. Fersman, L. Mokrushin, P. Pettersson, and W. Yi, \u201cTimes: A tool for modelling and implementation of embedded systems,\u201d The 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2002, Grenoble, France, April 8-12, 2002, vol.2280, pp.460-464, Springer-Verlag, 2002. 10.1007\/3-540-46002-0_32","DOI":"10.1007\/3-540-46002-0_32"},{"key":"10","doi-asserted-by":"publisher","unstructured":"[10] R. Alur and D.L. Dill, \u201cA theory of timed automata,\u201d Theoretical computer science, vol.126, no.2, pp.183-235, 1994. 10.1016\/0304-3975(94)90010-8","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"11","doi-asserted-by":"crossref","unstructured":"[11] A. David, J. Illum, K.G. Larsen, and A. Skou, \u201cModel-based framework for schedulability analysis using uppaal 4.1,\u201d Model-based design for embedded systems, vol.1, no.1, pp.93-119, 2009. 10.1201\/9781420067859-c4","DOI":"10.1201\/9781420067859-c4"},{"key":"12","doi-asserted-by":"crossref","unstructured":"[12] M. \u00c5sberg, P. Pettersson, and T. Nolte, \u201cModelling, verification and synthesis of two-tier hierarchical fixed-priority preemptive scheduling,\u201d 2011 23rd Euromicro Conference on Real-Time Systems, pp.172-181, IEEE, 2011. 10.1109\/ecrts.2011.24","DOI":"10.1109\/ECRTS.2011.24"},{"key":"13","doi-asserted-by":"crossref","unstructured":"[13] E. Pak, Y.-M. Ha, J. Park, Y. Kim, M. Song, and T. Kim, \u201cSyndicate: Software platform for distributed real-time system,\u201d 2015 IEEE 21st Pacific Rim International Symposium on Dependable Computing (PRDC), pp.327-328, IEEE, 2015. 10.1109\/prdc.2015.39","DOI":"10.1109\/PRDC.2015.39"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E100.D\/10\/E100.D_2017EDL8090\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T23:37:11Z","timestamp":1750894631000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E100.D\/10\/E100.D_2017EDL8090\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":13,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2017]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2017edl8090","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"type":"print","value":"0916-8532"},{"type":"electronic","value":"1745-1361"}],"subject":[],"published":{"date-parts":[[2017]]}}}