{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T12:24:35Z","timestamp":1780316675205,"version":"3.54.1"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319254227","type":"print"},{"value":"9783319254234","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25423-4_12","type":"book-chapter","created":{"date-parts":[[2015,11,30]],"date-time":"2015-11-30T17:10:46Z","timestamp":1448903446000},"page":"187-200","source":"Crossref","is-referenced-by-count":3,"title":["Model Checking $$\\mu $$ \u03bc C\/OS-III Multi-task System with TMSVL"],"prefix":"10.1007","author":[{"given":"Jin","family":"Cui","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Conghao","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,12,1]]},"reference":[{"issue":"4","key":"12_CR1","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1016\/j.tcs.2005.11.018","volume":"354","author":"Y Abdedda\u0131m","year":"2006","unstructured":"Abdedda\u0131m, Y., Asarin, E., Maler, O.: Scheduling with timed automata. Theoret. Comput. Sci. 354(4), 272\u2013300 (2006)","journal-title":"Theoret. Comput. Sci."},{"issue":"4","key":"12_CR2","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1109\/TASE.2010.2050199","volume":"7","author":"HB Mokadem","year":"2010","unstructured":"Mokadem, H.B., Berard, B., Gourcuff, V., De Smet, O., Roussel, J.-M.: Verification of a timed multitask system with uppaal. IEEE Trans. Autom. Sci. Eng. 7(4), 921\u2013932 (2010)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"issue":"11","key":"12_CR3","doi-asserted-by":"publisher","first-page":"1462","DOI":"10.1109\/TC.2004.103","volume":"53","author":"E Bini","year":"2004","unstructured":"Bini, E., Buttazzo, G.C.: Schedulability analysis of periodic fixed priority systems. IEEE Trans. Comput. 53(11), 1462\u20131473 (2004)","journal-title":"IEEE Trans. Comput."},{"issue":"7","key":"12_CR4","doi-asserted-by":"publisher","first-page":"933","DOI":"10.1109\/TC.2003.1214341","volume":"52","author":"E Bini","year":"2003","unstructured":"Bini, E., Buttazzo, G.C., Buttazzo, G.M.: Rate monotonic analysis: the hyperbolic bound. IEEE Trans. Comput. 52(7), 933\u2013942 (2003)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"12_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1109\/TSE.2004.1265815","volume":"30","author":"G Bucci","year":"2004","unstructured":"Bucci, G., Fedeli, A., Sassoli, L., Vicario, E.: Timed state space analysis of real-time preemptive systems. IEEE Trans. Softw. Eng. 30(2), 97\u2013111 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-88194-0_12","volume-title":"Formal Methods and Software Engineering","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C.: A unified model checking approach with projection temporal logic. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 167\u2013186. Springer, Heidelberg (2008)"},{"issue":"1","key":"12_CR7","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.scico.2007.09.001","volume":"70","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31\u201361 (2008)","journal-title":"Sci. Comput. Program."},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-34281-3_20","volume-title":"Formal Methods and Software Engineering","author":"M Han","year":"2012","unstructured":"Han, M., Duan, Z., Wang, X.: Time constraints with temporal logic programming. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 266\u2013282. Springer, Heidelberg (2012)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-41202-8_12","volume-title":"Formal Methods and Software Engineering","author":"Y Huang","year":"2013","unstructured":"Huang, Y., Ferreira, J.F., He, G., Qin, S., He, J.: Deadline analysis of AUTOSAR OS periodic tasks in the presence of interrupts. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 165\u2013181. Springer, Heidelberg (2013)"},{"key":"12_CR10","volume-title":"uC\/OS-III: The Real-Time Kernel","author":"JJ Labrosse","year":"2009","unstructured":"Labrosse, J.J.: uC\/OS-III: The Real-Time Kernel. Micrium Press, Weston (2009)"},{"issue":"1","key":"12_CR11","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/321738.321743","volume":"20","author":"CL Liu","year":"1973","unstructured":"Liu, C.L., Layland, J.W.: Scheduling algorithms for multiprogramming in a hard-real-time environment. J. ACM (JACM) 20(1), 46\u201361 (1973)","journal-title":"J. ACM (JACM)"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Madl, G., Dutt, N., Abdelwahed, S.: A conservative approximation method for the verification of preemptive scheduling using timed automata. In: 2009 15th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2009, pp. 255\u2013264 (2009)","DOI":"10.1109\/RTAS.2009.32"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Miku00ionis, M., Larsen, K.G., Rasmussen, J.I., Nielsen, B., Skou, A., Palm, S.U., Pedersen, J.S., Hougaard, P.: Schedulability analysis using uppaal: Herschel-planck case study. In: Proceedings of the 4th International Conference on Leveraging Applications of Formal Methods, Verification, and Validation - Volume Part II (2010)","DOI":"10.1007\/978-3-642-16561-0_21"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Pang, T., Duan, Z., Tian, C.: Symbolic model checking for propositional projection temporal logic. In: 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 9\u201316. IEEE (2012)","DOI":"10.1109\/TASE.2012.35"},{"issue":"3","key":"12_CR15","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1016\/j.ejor.2007.05.046","volume":"188","author":"RV Rasmus","year":"2008","unstructured":"Rasmus, R.V., Trick, M.A.: Round robin scheduling-a survey. Eur. J. Oper. Res. 188(3), 617\u2013636 (2008)","journal-title":"Eur. J. Oper. Res."},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-540-79228-4_4","volume-title":"Theory and Applications of Models of Computation","author":"C Tian","year":"2008","unstructured":"Tian, C., Duan, Z.: Propositional Projection Temporal Logic, B\n                    \n                      \n                    \n                    $${\\ddot{u}}$$\n                    \n                      \n                        \n                          u\n                          \u00a8\n                        \n                      \n                    \n                  chi Automata and \n                    \n                      \n                    \n                    $$\\omega $$\n                    \n                      \n                        \u03c9\n                      \n                    \n                  -Regular Expressions. In: Agrawal, M., Du, D.-Z., Duan, Z., Li, A. (eds.) TAMC 2008. LNCS, vol. 4978, pp. 47\u201358. Springer, Heidelberg (2008)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Wasziwoski, L., Hanzalek, Z.: Model checking of multitasking real-time applications based on the timed automata model using one clock. Behavioral Modeling for Embedded Systems and Technologies: Applications for Design and Implementation: Applications for Design and Implementation, p. 194 (2009)","DOI":"10.4018\/978-1-60566-750-8.ch008"},{"issue":"10","key":"12_CR18","doi-asserted-by":"publisher","first-page":"1678","DOI":"10.1016\/j.jss.2009.04.042","volume":"82","author":"L Waszniowski","year":"2009","unstructured":"Waszniowski, L., Kr\u00e1kora, J., Hanz\u00e1lek, Z.: Case study on distributed and fault tolerant system modeling based on timed automata. J. Syst. Softw. 82(10), 1678\u20131694 (2009)","journal-title":"J. Syst. Softw."}],"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-319-25423-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:05:26Z","timestamp":1559329526000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25423-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319254227","9783319254234"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25423-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}