{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T15:22:59Z","timestamp":1726068179896},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030414177"},{"type":"electronic","value":"9783030414184"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"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":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-41418-4_5","type":"book-chapter","created":{"date-parts":[[2020,2,19]],"date-time":"2020-02-19T01:14:01Z","timestamp":1582074841000},"page":"61-72","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Approach to Modeling and Verifying Multi-level Interrupt Systems with TMSVL"],"prefix":"10.1007","author":[{"given":"Jin","family":"Cui","sequence":"first","affiliation":[]},{"given":"Xu","family":"Lu","sequence":"additional","affiliation":[]},{"given":"Buwen","family":"Liang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,2,20]]},"reference":[{"key":"5_CR1","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":"9","key":"5_CR2","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1109\/2.58215","volume":"23","author":"JM Wing","year":"1990","unstructured":"Wing, J.M.: A specifier\u2019s introduction to formal methods. Computer 23(9), 8\u201322 (1990)","journal-title":"Computer"},{"issue":"2","key":"5_CR3","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":"1","key":"5_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2430536.2430537","volume":"22","author":"J Sun","year":"2013","unstructured":"Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., Andr\u00e9, \u00c9.: Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans. Softw. Eng. Methodol. 22(1), 1\u201329 (2013)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"2","key":"5_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.ic.2009.10.004","volume":"208","author":"P Bouyer","year":"2010","unstructured":"Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97\u2013116 (2010)","journal-title":"Inf. Comput."},{"key":"5_CR6","volume-title":"Principles of Model Checking","author":"JP Katoen","year":"2008","unstructured":"Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"5_CR7","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"JH Gallier","year":"2015","unstructured":"Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Courier Dover Publications, Mineola (2015)"},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1016\/j.tcs.2012.01.026","volume":"497","author":"Z Duan","year":"2013","unstructured":"Duan, Z., Zhang, N., Koutny, M.: A complete proof system for propositional projection temporal logic. Theor. Comput. Sci. 497, 84\u2013107 (2013)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR9","first-page":"35","volume":"37","author":"H Wang","year":"2017","unstructured":"Wang, H., Duan, Z., Tian, C.: Model checking multi-agent systems with APTL. Adhoc Sens. Wirel. Netw. 37, 35\u201352 (2017)","journal-title":"Adhoc Sens. Wirel. Netw."},{"key":"5_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking, vol. 10. Springer, Heidelberg (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10575-8"},{"key":"5_CR11","first-page":"1670","volume":"29","author":"J Cui","year":"2018","unstructured":"Cui, J., Duan, Z., Tian, C., Zhang, N.: Modeling and analysis of nested interrupt systems. J. Softw. 29, 1670\u20131680 (2018)","journal-title":"J. Softw."},{"issue":"3","key":"5_CR12","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s11704-015-3251-x","volume":"9","author":"Y Huang","year":"2015","unstructured":"Huang, Y., He, J., Zhu, H., Zhao, Y., Shi, J., Qin, S.: Semantic theories of programs with nested interrupts. Front. Comput. Sci. 9(3), 331\u2013345 (2015)","journal-title":"Front. Comput. Sci."},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-319-41540-6_4","volume-title":"Computer Aided Verification","author":"F Xu","year":"2016","unstructured":"Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z.: A practical verification framework for preemptive OS kernels. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 59\u201379. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41540-6_4"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-642-45293-2_5","volume-title":"Advanced Parallel Processing Technologies","author":"G Hou","year":"2013","unstructured":"Hou, G., Zhou, K., Chang, J., Li, R., Li, M.: Interrupt modeling and verification for embedded systems based on time petri nets. In: Wu, C., Cohen, A. (eds.) APPT 2013. LNCS, vol. 8299, pp. 62\u201376. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-45293-2_5"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Liu, H., Zhang, H., Jiang, Y., Song, X., Gu, M., Sun, J.: iDola: bridge modeling to verification and implementation of interrupt-driven systems. In: Theoretical Aspects of Software Engineering Conference, pp. 193\u2013200. IEEE (2014)","DOI":"10.1109\/TASE.2014.33"},{"issue":"11","key":"5_CR16","doi-asserted-by":"publisher","first-page":"118101","DOI":"10.1007\/s11432-015-0882-6","volume":"59","author":"N Zhang","year":"2016","unstructured":"Zhang, N., Duan, Z., Tian, C.: Model checking concurrent systems with MSVL. Sci. China Inf. Sci. 59(11), 118101 (2016)","journal-title":"Sci. China Inf. Sci."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Pan, M., Chen, S., Pei, Y., Zhang, T., Li, X.: Easy modelling and verification of unpredictable and preemptive interrupt-driven systems. In: Proceedings of the 41st International Conference on Software Engineering, pp. 212\u2013222. IEEE Press (2019)","DOI":"10.1109\/ICSE.2019.00037"},{"issue":"2","key":"5_CR18","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1109\/TR.2018.2806349","volume":"67","author":"J Cui","year":"2018","unstructured":"Cui, J., Duan, Z., Tian, C., Du, H., Zhang, N.: A novel approach to modeling and verifying real-time systems for high reliability. IEEE Trans. Reliab. 67(2), 481\u2013493 (2018)","journal-title":"IEEE Trans. Reliab."},{"key":"5_CR19","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-88194-0_12"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"1101","DOI":"10.1109\/TR.2018.2876333","volume":"68","author":"M Wang","year":"2018","unstructured":"Wang, M., Tian, C., Zhang, N., Duan, Z.: Verifying full regular temporal properties of programs via dynamic program execution. IEEE Trans. Reliab. 68, 1101\u20131116 (2018)","journal-title":"IEEE Trans. Reliab."},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jpdc.2017.09.003","volume":"118","author":"B Yu","year":"2018","unstructured":"Yu, B., Duan, Z., Tian, C., Zhang, N.: Verifying temporal properties of programs: a parallel approach. J. Parallel Distrib. Comput. 118, 89\u201399 (2018)","journal-title":"J. Parallel Distrib. Comput."},{"key":"5_CR22","volume-title":"Temporal Logic and Temporal Logic Programming","author":"Z Duan","year":"2005","unstructured":"Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2005)"},{"key":"5_CR23","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2017.07.032","volume":"749","author":"K Yang","year":"2018","unstructured":"Yang, K., Duan, Z., Tian, C., Zhang, N.: A compiler for MSVL and its applications. Theor. Comput. Sci. 749, 2\u201316 (2018)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-41418-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,19]],"date-time":"2020-02-19T01:14:25Z","timestamp":1582074865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-41418-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030414177","9783030414184"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-41418-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"20 February 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SOFL+MSVL","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Structured Object-Oriented Formal Language and Method","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Shenzhen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sofl2019a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/csse.szu.edu.cn\/icfem2019\/soflmsvl.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}