{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T13:22:20Z","timestamp":1725974540274},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319901039"},{"type":"electronic","value":"9783319901046"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-90104-6_4","type":"book-chapter","created":{"date-parts":[[2018,4,17]],"date-time":"2018-04-17T12:53:22Z","timestamp":1523969602000},"page":"51-68","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Boosting Uppaal for OSEK\/VDX Applications with a Sequentialization Approach"],"prefix":"10.1007","author":[{"given":"Haitao","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhuo","family":"Cheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianxin","family":"Xue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yonggang","family":"Lu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,18]]},"reference":[{"key":"4_CR1","unstructured":"Cimatti, A., Micheli, A., Narasamdya, I., Roveri, M.: Verifying SystemC: a software model checking approach. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 51\u201359 (2010)"},{"issue":"11","key":"4_CR2","first-page":"117","volume":"58","author":"B Armin","year":"2003","unstructured":"Armin, B., Clarke, E.M., Zhu, Y.: Bounded model checking. Adv. Comput. 58(11), 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: 17th IEEE Real-Time Systems Symposium, p. 73 (1996)","DOI":"10.1109\/REAL.1996.563702"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03359-9_2"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-22306-8_7","volume-title":"Model Checking Software","author":"D Campana","year":"2011","unstructured":"Campana, D., Cimatti, A., Narasamdya, I., Roveri, M.: An analytic evaluation of SystemC encodings in promela. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol. 6823, pp. 90\u2013107. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22306-8_7"},{"issue":"11","key":"4_CR6","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"152","author":"EM Clarke","year":"2009","unstructured":"Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 152(11), 74\u201384 (2009)","journal-title":"Commun. ACM"},{"issue":"5","key":"4_CR7","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35746-6_1","volume-title":"Tools for Practical Software Verification","author":"EM Clarke","year":"2012","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1\u201330. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-35746-6_1"},{"key":"4_CR9","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. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"4_CR10","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Lucent Technologies Inc., Bell Laboratories, Boston (2003)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Zhang, H., Aoki, T., Lin, X., et al.: SMT-based bounded model checking for OSEK\/VDX applications. In: 20th Asia-Pacific Software Engineering Conference, pp. 307\u2013314 (2013)","DOI":"10.1109\/APSEC.2013.49"},{"key":"4_CR12","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-319-17581-2_16","volume-title":"Formal Techniques for Safety-Critical Systems","author":"H Zhang","year":"2015","unstructured":"Zhang, H., Aoki, T., Chiba, Y.: A spin-based approach for checking OSEK\/VDX applications. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 239\u2013255. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-17581-2_16"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Bechennec, J., Briday, M., Faucou, S., et al.: Trampoline-an open source implementation of the OSEK\/VDX RTOS specification. In: 11th International Conference on Emerging Technologies and Factory Automation, September 2006","DOI":"10.1109\/ETFA.2006.355432"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Chen, J., Aoki, T.: Conformance testing for OSEK\/VDX operating system using model checking. In: Proceedings of the 18th Asia-Pacific Software Engineering Conference, pp. 274\u2013281 (2011)","DOI":"10.1109\/APSEC.2011.26"},{"key":"4_CR15","volume-title":"Programming in the OSEK\/VDX Environment","author":"J Lemieux","year":"2001","unstructured":"Lemieux, J.: Programming in the OSEK\/VDX Environment. CMP, Lawrence (2001)"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-642-54862-8_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Morse","year":"2014","unstructured":"Morse, J., Ramalho, M., Cordeiro, L., Nicole, D., Fischer, B.: ESBMC 1.22. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 405\u2013407. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54862-8_31"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-24559-6_12","volume-title":"Formal Methods and Software Engineering","author":"J Sun","year":"2011","unstructured":"Sun, J., Liu, Y., Song, S., Dong, J.S., Li, X.: PRTS: an approach for model checking probabilistic real-time hierarchical systems. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 147\u2013162. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-24559-6_12"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B.: Verifying multi-threaded software using SMT-based context-bounded model checking. In: The International Conference on Software Engineering (ICSE), pp. 331\u2013340, May 2011","DOI":"10.1145\/1985793.1985839"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-54862-8_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Inverso","year":"2014","unstructured":"Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Lazy-CSeq: a lazy sequentialization tool for C. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 398\u2013401. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54862-8_29"},{"issue":"10","key":"4_CR21","doi-asserted-by":"publisher","first-page":"1678","DOI":"10.1016\/j.jss.2009.04.042","volume":"82","author":"W Libor","year":"2009","unstructured":"Libor, W., Jan, K., Zdenek, H.: 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."},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Choi, Y.: Safety analysis of trampoline os using model checking: an experience report. In: Proceedings of the IEEE 22nd International Symposium on Software Reliability Engineering, pp. 200\u2013209, November 2011","DOI":"10.1109\/ISSRE.2011.22"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Huang, Y., Zhao, Y., Zhu, L., et al.: Modeling and verifying the code-level OSEK\/VDX operating system with CSP. In: Fifth International Symposium on Theoretical Aspects of Software Engineering, pp. 142\u2013149 (2011)","DOI":"10.1109\/TASE.2011.11"},{"issue":"1","key":"4_CR24","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/314602.314605","volume":"21","author":"Z Liu","year":"1999","unstructured":"Liu, Z., Joseph, M.: Specification and verification of fault-tolerance, timing, and scheduling. ACM Trans. Program. Lang. Syst. 21(1), 46\u201389 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."}],"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-90104-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,17]],"date-time":"2018-04-17T12:55:36Z","timestamp":1523969736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-90104-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319901039","9783319901046"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-90104-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}