{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:33:13Z","timestamp":1742938393476,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319312194"},{"type":"electronic","value":"9783319312200"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-31220-0_2","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T08:59:52Z","timestamp":1457773192000},"page":"15-28","source":"Crossref","is-referenced-by-count":0,"title":["Modeling and Verification of an Interrupt System in $$\\mu $$ \u03bc C\/OS-III with TMSVL"],"prefix":"10.1007","author":[{"given":"Jin","family":"Cui","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"2_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"12","key":"2_CR2","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume":"4","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. Lect. Notes Comput. Sci. 4(12), 200\u2013236 (2004)","journal-title":"Lect. Notes Comput. Sci."},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/BFb0055357","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"M Bozga","year":"1998","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: KRONOS: a model-checking tool for real-time systems (Tool-presentation for FTRTFT 1998). In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 298\u2013302. Springer, Heidelberg (1998)"},{"issue":"1","key":"2_CR4","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1002\/stvr.1482","volume":"24","author":"Y Choi","year":"2014","unstructured":"Choi, Y.: Model checking trampoline OS: a case study on safety analysis for automotive software. Softw. Test. Verif. Reliab. 24(1), 38\u201360 (2014)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"2_CR5","first-page":"1","volume-title":"Structured Programming","author":"EW Dijkstra","year":"1972","unstructured":"Dijkstra, E.W.: Notes on structured programming. Structured Programming, pp. 1\u201382. Academic Press Ltd., New York (1972)"},{"key":"2_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., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 167\u2013186. Springer, Heidelberg (2008)"},{"issue":"1","key":"2_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":"2_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)"},{"issue":"3","key":"2_CR9","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1145\/356651.356652","volume":"7","author":"JC Huang","year":"1975","unstructured":"Huang, J.C.: An approach to program testing. ACM Comput. Surv. (CSUR) 7(3), 113\u2013128 (1975)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"2_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)"},{"key":"2_CR11","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"issue":"1","key":"2_CR12","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1023\/A:1021701221847","volume":"24","author":"K Lundqvist","year":"2003","unstructured":"Lundqvist, K., Asplund, L.: A ravenscar-compliant run-time kernel for safety-critical systems. Real-Time Syst. 24(1), 29\u201354 (2003)","journal-title":"Real-Time Syst."},{"issue":"1","key":"2_CR13","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/s11704-009-0073-8","volume":"4","author":"M Lv","year":"2010","unstructured":"Lv, M., Guan, N., Deng, Q., Ge, Y., Wang, Y.: Static worst-case execution time analysis of the $$\\mu $$ \u03bc C\/OS-II real-time kernel. Front. Comput. Sci. China 4(1), 17\u201327 (2010)","journal-title":"Front. Comput. Sci. China"},{"issue":"1","key":"2_CR14","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s11241-007-9036-z","volume":"38","author":"L Waszniowski","year":"2008","unstructured":"Waszniowski, L., Hanzlek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38(1), 39\u201365 (2008)","journal-title":"Real-Time Syst."},{"issue":"10","key":"2_CR15","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","Structured Object-Oriented Formal Language and Method"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-31220-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2016,10,6]],"date-time":"2016-10-06T07:00:48Z","timestamp":1475737248000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-31220-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319312194","9783319312200"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-31220-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}