{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:31:28Z","timestamp":1759638688534,"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_8","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T08:59:52Z","timestamp":1457773192000},"page":"103-117","source":"Crossref","is-referenced-by-count":4,"title":["Model Checking Process Scheduling over Multi-core Computer System with MSVL"],"prefix":"10.1007","author":[{"given":"Xinfeng","family":"Shu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"5","key":"8_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/s10009-009-0110-9","volume":"11","author":"A Wijs","year":"2009","unstructured":"Wijs, A., van de Pol, J., Bortnik, E.M.: Solving scheduling problems by untimed model checking. STTT 11(5), 375\u2013392 (2009)","journal-title":"STTT"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44829-2_1","volume-title":"Model Checking Software","author":"TC Ruys","year":"2003","unstructured":"Ruys, T.C.: Optimal scheduling using branch and bound with SPIN 4.0. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 1\u201317. Springer, Heidelberg (2003)"},{"issue":"2","key":"8_CR3","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/s11241-008-9059-0","volume":"41","author":"D Lime","year":"2009","unstructured":"Lime, D., Roux, O.H.: Formal verification of real-time systems with preemptive scheduling. Real-Time Syst. 41(2), 118\u2013151 (2009)","journal-title":"Real-Time Syst."},{"key":"8_CR4","unstructured":"Duan, Z.: An extended interval temporal logic and a framing technique for interval temporal logic programming. Ph.D. thesis, University of Newcastle Upon Tyne, May 1996"},{"key":"8_CR5","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)"},{"issue":"1","key":"8_CR6","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","volume":"45","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Inf. 45(1), 43\u201378 (2008)","journal-title":"Acta Inf."},{"issue":"18","key":"8_CR7","doi-asserted-by":"publisher","first-page":"1729","DOI":"10.1016\/j.tcs.2010.12.047","volume":"412","author":"C Tian","year":"2011","unstructured":"Tian, C., Duan, Z.: Expressiveness of propositional projection temporal logic with star. Theor. Comput. Sci. 412(18), 1729\u20131744 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR8","first-page":"333","volume":"19","author":"Z Duan","year":"2004","unstructured":"Duan, Z., Koutny, M.: A Framed Temporal Logic Programming Language. J. Comput. Sci. Technol. 19, 333\u2013344 (2004)","journal-title":"J. Comput. Sci. Technol."},{"issue":"1","key":"8_CR9","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":"8_CR10","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)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Wang, M., Duan, Z., Tian, C.: Simulation and verification of the virtual memory management system with MSVL. In: Proceedings of the 2014 IEEE 18th International Conference on Computer Supported Cooperative Work in Design (CSCWD), pp. 360\u2013365, May 2014","DOI":"10.1109\/CSCWD.2014.6846870"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-319-25423-4_12","volume-title":"Formal Methods and Software Engineering","author":"J Cui","year":"2015","unstructured":"Cui, J., Duan, Z., Tian, C., Zhang, N., Zhou, C.: Model Checking \n                      \n                        \n                      \n                      $$\\mu $$\n                      \n                        \n                          \u03bc\n                        \n                      \n                     C\/OS-III Multi-task System with TMSVL. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) Formal Methods and Software Engineering. Lecture Notes in Computer Science, vol. 9407, pp. 187\u2013200. Springer, Switzerland (2015)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-39277-1_7","volume-title":"Structured Object-Oriented Formal Language and Method","author":"Y Yu","year":"2013","unstructured":"Yu, Y., Duan, Z., Tian, C., Yang, M.: Model checking C programs with MSVL. In: Liu, S. (ed.) SOFL 2012. LNCS, vol. 7787, pp. 87\u2013103. Springer, Heidelberg (2013)"},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/j.entcs.2014.12.006","volume":"309","author":"Y Bin","year":"2014","unstructured":"Bin, Y., Duan, Z., Tian, C.: Bounded model checking of traffic light control system. Electr. Notes Theor. Comput. Sci. 309, 63\u201374 (2014)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"8_CR15","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/s00165-014-0303-1","volume":"27","author":"Q Ma","year":"2015","unstructured":"Ma, Q., Duan, Z., Zhang, N., Wang, X.: Verification of distributed systems with the axiomatic system of MSVL. Formal Asp. Comput. 27(1), 103\u2013131 (2015)","journal-title":"Formal Asp. Comput."}],"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-319-31220-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T14:24:32Z","timestamp":1559399072000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-31220-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319312194","9783319312200"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-31220-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}