{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T11:50:07Z","timestamp":1649073007133},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"S2","license":[{"start":{"date-parts":[[2018,2,1]],"date-time":"2018-02-01T00:00:00Z","timestamp":1517443200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Cluster Comput"],"published-print":{"date-parts":[[2019,3]]},"DOI":"10.1007\/s10586-017-1319-0","type":"journal-article","created":{"date-parts":[[2018,2,1]],"date-time":"2018-02-01T15:14:07Z","timestamp":1517498047000},"page":"2543-2554","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["An improved formalization analysis approach to determine schedulability of global multiprocessor scheduling based on symbolic safety analysis and statistical model checking in smartphone systems"],"prefix":"10.1007","volume":"22","author":[{"given":"Haibin","family":"Cai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hao","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,2,1]]},"reference":[{"issue":"4","key":"1319_CR1","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1145\/1978802.1978814","volume":"43","author":"RI Davis","year":"2011","unstructured":"Davis, R.I., Burns, A.: A survey of hard real-time scheduling for multiprocessor systems. ACM Comput. Surv. 43(4), 35 (2011)","journal-title":"ACM Comput. Surv."},{"key":"1319_CR2","unstructured":"Tindell, K.: Adding time-offsets to schedulability analysis. Technical report, University of York (1994)"},{"key":"1319_CR3","doi-asserted-by":"crossref","unstructured":"Yomsi, P.M., Bertrand, D., Navet, N., Davis, R.L.: Controller area network (CAN): response time analysis with offsets. In: WFCS, pp. 43\u201352 (2012)","DOI":"10.1109\/WFCS.2012.6242539"},{"key":"1319_CR4","doi-asserted-by":"crossref","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. Lecture Notes in Computer Science, vol. 2791, pp. 60\u201372. Springer (2003)","DOI":"10.1007\/978-3-540-40903-8_6"},{"key":"1319_CR5","doi-asserted-by":"crossref","unstructured":"Fersman, E., Mokrushin, L., Petersson, P., Wang, Y.: Schedulability analysis of fixed-priority systems using timed automata. Theor. Comput. Sci. 354(2), 301\u2013317","DOI":"10.1016\/j.tcs.2005.11.019"},{"issue":"1","key":"1319_CR6","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s11241-007-9036-z","volume":"38","author":"L Waszniowski","year":"2008","unstructured":"Waszniowski, L., Hanzalek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38(1), 39\u201365 (2008)","journal-title":"Real-Time Syst."},{"key":"1319_CR7","unstructured":"UPPAAL HELP. \n                    http:\/\/www.uppaal.org\/\n                    \n                   (2016)"},{"key":"1319_CR8","doi-asserted-by":"crossref","unstructured":"Cicirelli, F., Furfaro, A., Nigro, L., Pupo, F.: Development of a schedulability analysis framework based on ptpn and uppaal with stopwatches. In: Boukerche, A., Cahill, V., El-Saddik, A., Theodoropoulos, G.K., Walshe, R. (eds.) DS-RT:57-64. IEEE Computer Society (2012)","DOI":"10.1109\/DS-RT.2012.16"},{"issue":"1\u20132","key":"1319_CR9","first-page":"1","volume":"77","author":"B Aske Wiid","year":"2008","unstructured":"Aske Wiid, B., Hansen, M.R., Madsen, J.: Models and formal verification of multiprocessor system-on-chips. J. Log. Algebraic Program. 77(1\u20132), 1\u201319 (2008)","journal-title":"J. Log. Algebraic Program."},{"key":"1319_CR10","doi-asserted-by":"crossref","unstructured":"David, A., Illum, J., Larsen, K.G., Skou, A.: Model-based framework for schedulability analysis using uppaal 4.1. In: Model-based Design for Embedded Systems, pp. 93\u2013119 (2010)","DOI":"10.1201\/9781420067859-c4"},{"key":"1319_CR11","doi-asserted-by":"crossref","unstructured":"Baker, T.P., Cirinei, M.: Brute-force determination of multiprocessor schedulability for sets of sopradic hard-deadline tasks. In: Tovar, E., Tsigas, P., Fouchal, H. (eds.) OPODIS, vol. 4878, pp. 62\u201375. Springer (2007)","DOI":"10.1007\/978-3-540-77096-1_5"},{"key":"1319_CR12","doi-asserted-by":"crossref","unstructured":"Cordovilla, M., Boniol, F., Noulard, E., Pagetti, C.: Multiprocessor schedulability analyser. In: Chu, W.C., Wong, E.W., Palakal, M.J., Hung, C.-C. (eds.) SAC, pp. 735\u2013741. ACM (2011)","DOI":"10.1145\/1982185.1982345"},{"key":"1319_CR13","doi-asserted-by":"crossref","unstructured":"Boudjadar, A., David, A., Kim, J.H., Kim, L.G., Mikucionis, M., Nyman, U., Skou, A.: Hierarchical scheduling framework based on compositional analysis using UPPAAL. In: Fiadeiro, J.L. (ed.) Proceedings of the Formal Aspects of Component Software, pp. 61\u201378. Springer (2014)","DOI":"10.1007\/978-3-319-07602-7_6"},{"key":"1319_CR14","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M.: Schedulability of Herschel-Planck revisited using statistical model checking. In: Margaria, T. (ed.) Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, pp. 293\u2013307. Springer (2012)","DOI":"10.1007\/978-3-642-34032-1_28"},{"key":"1319_CR15","unstructured":"Oguzcan, O., Broenink, J.F., Mader, A.: Schedulability analysis of timed CSP models using the pat model checker. In: Communicating Process Architectures. Open Channel Publishing Ltd (2012)"},{"issue":"5","key":"1319_CR16","doi-asserted-by":"crossref","first-page":"638","DOI":"10.1109\/TSE.2012.54","volume":"39","author":"L Carnevali","year":"2013","unstructured":"Carnevali, L., Pinzuti, A., Vicario, E.: Compositional verification for hierarchical scheduling of real-time systems. IEEE Trans. Softw. Eng. 39(5), 638\u2013657 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1319_CR17","unstructured":"Ericsson, C., Wall, A., Yi, W.: Timed automata as task models for event-driven systems. In: Proceedings of Nordic Workshop on Programming Theory (1998)"},{"key":"1319_CR18","doi-asserted-by":"crossref","unstructured":"Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processed: schedulability and decidability. In: Proceedings of TACAS02. LNCS, vol. 2280, pp. 67\u201382 (2002)","DOI":"10.1007\/3-540-46002-0_6"},{"key":"1319_CR19","doi-asserted-by":"publisher","unstructured":"Schmitz, M.T., Al-Hashimi, B.M., Eles, P.: System-Level Design Techniques for Energy-Efficient Embedded Systems. Springer (2004). \n                    https:\/\/doi.org\/10.1007\/b106642","DOI":"10.1007\/b106642"},{"key":"1319_CR20","doi-asserted-by":"crossref","unstructured":"Clarke, EM., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Proceedings of the 9th International Conference on Automated Technology for Verification and Analysis (ATVA\u201911), pp. 1\u201312. Taipei, Taiwan, 11\u201314 Oct 2011","DOI":"10.1007\/978-3-642-24372-1_1"},{"issue":"2","key":"1319_CR21","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/s10009-014-0331-4","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M.: Schedulability of Herschel revisited using statistical model checking. Int. J. Softw. Tools Technol. Transf. 17(2), 187\u2013199 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1319_CR22","doi-asserted-by":"crossref","unstructured":"Christensen, S., Kristensen, L., Mailund, T.: A sweep-line method for state space exploration. In: TACAS, pp. 450\u2013464 (2001)","DOI":"10.1007\/3-540-45319-9_31"},{"key":"1319_CR23","doi-asserted-by":"crossref","unstructured":"Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR. Lecture Notes in Computer Science, vol. 1877, pp. 138\u2013152 (2000)","DOI":"10.1007\/3-540-44618-4_12"}],"container-title":["Cluster Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10586-017-1319-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-017-1319-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-017-1319-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,25]],"date-time":"2019-10-25T21:04:57Z","timestamp":1572037497000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10586-017-1319-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,1]]},"references-count":23,"journal-issue":{"issue":"S2","published-print":{"date-parts":[[2019,3]]}},"alternative-id":["1319"],"URL":"https:\/\/doi.org\/10.1007\/s10586-017-1319-0","relation":{},"ISSN":["1386-7857","1573-7543"],"issn-type":[{"value":"1386-7857","type":"print"},{"value":"1573-7543","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,2,1]]},"assertion":[{"value":"4 September 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 October 2017","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 October 2017","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 February 2018","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}