{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T15:25:24Z","timestamp":1759937124754},"publisher-location":"Cham","reference-count":9,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319064093"},{"type":"electronic","value":"9783319064109"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06410-9_48","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T21:03:01Z","timestamp":1397854981000},"page":"718-732","source":"Crossref","is-referenced-by-count":4,"title":["Formal Verification of Lunar Rover Control Software Using UPPAAL"],"prefix":"10.1007","author":[{"given":"Lijun","family":"Shan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuying","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ning","family":"Fu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xingshe","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lei","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lijng","family":"Wan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lei","family":"Qiao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianxin","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"48_CR1","doi-asserted-by":"crossref","unstructured":"Lee, E.A.: Cyber Physical Systems: Design Challenges. In: 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing (ISORC), pp. 363\u2013369 (2008)","DOI":"10.1109\/ISORC.2008.25"},{"key":"48_CR2","unstructured":"Gluck, P.R., Holzmann, G.J.: Using SPIN model checking for flight software verification. In: Aerospace Conference Proceedings. IEEE (2002)"},{"key":"48_CR3","unstructured":"Behrmann, G., David, A., Larsen, K.G., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: Third International Conference on Quantitative Evaluation of Systems (QEST 2006). IEEE (2006)"},{"key":"48_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-642-28891-3_39","volume-title":"NASA Formal Methods","author":"P. Bulychev","year":"2012","unstructured":"Bulychev, P., David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Checking and distributing statistical model checking. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 449\u2013463. Springer, Heidelberg (2012)"},{"key":"48_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A. Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: An overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 122\u2013135. Springer, Heidelberg (2010)"},{"key":"48_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-642-34032-1_28","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies","author":"A. David","year":"2012","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M.: Schedulability of herschel-planck revisited using statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol.\u00a07610, pp. 293\u2013307. Springer, Heidelberg (2012)"},{"issue":"1","key":"48_CR7","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1023\/A:1007993819750","volume":"14","author":"C.J. Fidge","year":"1998","unstructured":"Fidge, C.J.: Real-time schedulability tests for preemptive multitasking. Real-Time Systems\u00a014(1), 61\u201393 (1998)","journal-title":"Real-Time Systems"},{"issue":"1","key":"48_CR8","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s11241-007-9036-z","volume":"38","author":"L. Waszniowski","year":"2008","unstructured":"Waszniowski, L., Hanz\u00e1lek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Systems\u00a038(1), 39\u201365 (2008)","journal-title":"Real-Time Systems"},{"key":"48_CR9","unstructured":"Waszniowski, L., Hanzalek, Z.: Over-approximate model of multitasking application based on timed automata using only one clock. In: 19th IEEE International Parallel and Distributed Processing Symposium. IEEE (2005)"}],"container-title":["Lecture Notes in Computer Science","FM 2014: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06410-9_48","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T16:50:04Z","timestamp":1558889404000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06410-9_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319064093","9783319064109"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06410-9_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}