{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T02:52:22Z","timestamp":1763347942456,"version":"3.41.0"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319194578"},{"type":"electronic","value":"9783319194585"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19458-5_4","type":"book-chapter","created":{"date-parts":[[2015,5,11]],"date-time":"2015-05-11T11:41:14Z","timestamp":1431344474000},"page":"47-61","source":"Crossref","is-referenced-by-count":33,"title":["Formal Analysis and Testing of Real-Time Automotive Systems Using UPPAAL Tools"],"prefix":"10.1007","author":[{"given":"Jin Hyun","family":"Kim","sequence":"first","affiliation":[]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[]},{"given":"Brian","family":"Nielsen","sequence":"additional","affiliation":[]},{"given":"Marius","family":"Miku\u010dionis","sequence":"additional","affiliation":[]},{"given":"Petur","family":"Olsen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"AUTOSAR: Technical Overview. Standard, http:\/\/www.autosar.org"},{"key":"4_CR2","unstructured":"SAE International Architecture Analysis & Design Language (AADL) Standard, http:\/\/www.aadl.info\/aadl\/currentsite\/"},{"issue":"2","key":"4_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.\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Arun Chakrapani\u00a0Rao, M.G.D., Sethu, R.: Formal requirements analysis techniques for software-intensive automotive electronic control systems. Technical report (2011)","DOI":"10.4271\/2011-01-1002"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol.\u00a03185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J. Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol.\u00a03098, pp. 87\u2013124. Springer, Heidelberg (2004)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Miku\u010dionis, M., Poulsen, D.B., Legay, A., Wang, Z.: Uppaal-smc: Statistical model checking for priced timed automata. In: Wiklicky, H., Massink, M. (eds.) QAPL. EPTCS, vol.\u00a085, pp. 1\u201316 (2012)","DOI":"10.4204\/EPTCS.85.1"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-03240-0_2","volume-title":"Formal Methods for Industrial Critical Systems","author":"R. Cleaveland","year":"2009","unstructured":"Cleaveland, R.: Model-based verification of automotive control software. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol.\u00a05596, p. 2. Springer, Heidelberg (2009)"},{"key":"4_CR9","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)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Uppaal smc tutorial. International Journal on Software Tools for Technology Transfer, 1\u201319 (2015)","DOI":"10.1007\/s10009-014-0361-y"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Frehse, G., Hamann, A., Quinton, S., W\u00f6hrle, M.: Formal Analysis of Timing Effects on Closed-loop Properties of Control Software. In: 35th IEEE Real-Time Systems Symposium 2014 (RTSS), Rome, Italy (December 2014)","DOI":"10.1109\/RTSS.2014.28"},{"key":"4_CR12","unstructured":"IEC 61508: Functional Safety of Electrical\/Electronic\/Programmable Electronic Safety Related Systems. Standard, International Organization for Standardization, Geneva, CH (2010)"},{"key":"4_CR13","unstructured":"ISO 26262-6: Road vehicles \u2013 Functional safety \u2013 Part 6: Product development at the software level. Standard, International Organization for Standardization, Geneva, CH (2011)"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Jersak, M., Richter, K., Ernst, R., Braam, J.-C., Jiang, Z.-Y., Wolf, F.: Formal methods for integration of automotive software. In: Design, Automation and Test in Europe Conference and Exhibition, pp. 45\u201350 (2003)","DOI":"10.1109\/DATE.2003.1253804"},{"key":"4_CR15","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., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 122\u2013135. Springer, Heidelberg (2010)"},{"issue":"3","key":"4_CR16","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst.\u00a04(3), 455\u2013495 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"5","key":"4_CR17","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A.P. Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Asp. Comput.\u00a06(5), 495\u2013512 (1994)","journal-title":"Formal Asp. Comput."},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Tekaya, M., Bennani, M.T., Youssef, A.: Test case generation for automotive applications. In: 2014 World Symposium on Computer Applications Research (WSCAR), pp. 1\u20136 (January 2014)","DOI":"10.1109\/WSCAR.2014.6916809"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19458-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T22:49:27Z","timestamp":1748386167000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19458-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319194578","9783319194585"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19458-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}