{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,26]],"date-time":"2025-09-26T13:21:57Z","timestamp":1758892917914},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2017,8,11]],"date-time":"2017-08-11T00:00:00Z","timestamp":1502409600000},"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":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2018,5]]},"DOI":"10.1007\/s11432-016-9039-4","type":"journal-article","created":{"date-parts":[[2017,8,16]],"date-time":"2017-08-16T11:13:55Z","timestamp":1502882035000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["autoC: an efficient translator for model checking deterministic scheduler based OSEK\/VDX applications"],"prefix":"10.1007","volume":"61","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":"Guoqiang","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaoying","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,11]]},"reference":[{"key":"9039_CR1","volume-title":"Programming in the OSEK\/VDX Environment","author":"J Lemieux","year":"2011","unstructured":"Lemieux J. Programming in the OSEK\/VDX Environment. New York: CMP Media, Inc., 2011"},{"key":"9039_CR2","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"152","author":"E M Clarke","year":"2009","unstructured":"Clarke E M, Emerson E A, Sifakis J. Model checking: algorithmic verification and debugging. Commun ACM, 2009, 152: 74\u201384","journal-title":"Commun ACM"},{"key":"9039_CR3","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E M Clarke","year":"1994","unstructured":"Clarke E M, Grumberg O, Long D E. Model checking and abstraction. ACM Trans Programm Languages Syst, 1994, 16: 1512\u20131542","journal-title":"ACM Trans Programm Languages Syst"},{"key":"9039_CR4","doi-asserted-by":"crossref","first-page":"793","DOI":"10.1007\/s11432-007-0073-y","volume":"50","author":"F Pu","year":"2007","unstructured":"Pu F, Zhang W H. Combining search space partition and abstraction for LTL model checking. Sci China Ser F-Inf Sci, 2007, 50: 793\u2013810","journal-title":"Sci China Ser F-Inf Sci"},{"key":"9039_CR5","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G J Holzmann","year":"2003","unstructured":"Holzmann G J. The Spin Model Checker: Primer and Reference Manual. Boston: Lucent Technologies Inc., 2003"},{"key":"9039_CR6","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/978-3-642-54862-8_31","volume-title":"Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"J Morse","year":"2014","unstructured":"Morse J, Ramalho M, Cordeiro L, et al. ESBMC 1.22. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2014. 405\u2013407"},{"key":"9039_CR7","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen E, Dahlweid M, Hillebrand M, et al. VCC: a practical system for verifying concurrent C. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics. Berlin: Springer, 2009. 23\u201342"},{"key":"9039_CR8","first-page":"331","volume-title":"Proceedings of the 33rd International Conference on Software Engineering, Waikiki","author":"L Cordeiro","year":"2011","unstructured":"Cordeiro L, Fischer B. Verifying multi-threaded software using SMT-based context-bounded model checking. In: Proceedings of the 33rd International Conference on Software Engineering, Waikiki, 2011. 331\u2013340"},{"key":"9039_CR9","first-page":"51","volume-title":"Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, Lugano","author":"A Cimatti","year":"2010","unstructured":"Cimatti A, Micheli A, Narasamdya I, et al. Verifying SystemC: a software model checking approach. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, Lugano, 2010. 51\u201360"},{"key":"9039_CR10","first-page":"239","volume-title":"Proceedings of the 3rd International Workshop Formal Techniques for Safety-Critical Systems (FTSCS), Paris","author":"H T Zhang","year":"2014","unstructured":"Zhang H T, Aoki T, Chiba Y. A spin-based approach for checking OSEK\/VDX applications. In: Proceedings of the 3rd International Workshop Formal Techniques for Safety-Critical Systems (FTSCS), Paris, 2014. 239\u2013255"},{"key":"9039_CR11","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s11241-007-9036-z","volume":"38","author":"L Waszniowski","year":"2008","unstructured":"Waszniowski L, Hanzalek Z. Formal verification of multitasking applications based on timed automata model. J Real-Time Syst, 2008, 38: 39\u201365","journal-title":"J Real-Time Syst"},{"key":"9039_CR12","first-page":"1","volume-title":"Tools for Practical Software Verification. Berlin: Springer","author":"E M Clarke","year":"2012","unstructured":"Clarke E M, Klieber W, Novacek M, et al. Model checking and the state explosion problem. In: Tools for Practical Software Verification. Berlin: Springer, 2012. 1\u201330"},{"key":"9039_CR13","first-page":"1","volume-title":"Proceedings of the 8th International Conference on Software Testing, Verification and Validation, Graz","author":"H T Zhang","year":"2015","unstructured":"Zhang H T, Aoki T, Chiba Y. Yes! You can use your model checker to verify OSEK\/VDX applications. In: Proceedings of the 8th International Conference on Software Testing, Verification and Validation, Graz, 2015. 1\u201310"},{"key":"9039_CR14","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1007\/978-3-642-22306-8_7","volume-title":"Proceedings of the 18th International SPIN Conference on Model Checking Software, Snowbird","author":"D Campana","year":"2011","unstructured":"Campana D, Cimatti A, Narasamdya I, et al. An analytic evaluation of SystemC encodings in Promela. In: Proceedings of the 18th International SPIN Conference on Model Checking Software, Snowbird, 2011. 90\u2013107"},{"key":"9039_CR15","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/978-3-642-54862-8_29","volume-title":"Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Grenoble","author":"O Inverso","year":"2014","unstructured":"Inverso O, Tomasco E, Fischer B, et al. Lazy-CSeq: a lazy sequentialization tool for C. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Grenoble, 2014. 398\u2013401"},{"key":"9039_CR16","unstructured":"IEEE Standard for Information Technology. Portable operating system interface (POSIX) base specifications. Issue 7. http:\/\/standards.ieee.org\/reading\/ieee\/interp\/1003.1-2008.html"},{"key":"9039_CR17","volume-title":"Real-Time Systems and Programming Languages","author":"A Burns","year":"2009","unstructured":"Burns A, Wellings A. Real-Time Systems and Programming Languages. 4th ed. New York: AddisonWesley Longmain, 2009"},{"key":"9039_CR18","first-page":"213","volume-title":"Proceedings of the 11th International Conference on Compiler Construction","author":"C N George","year":"2002","unstructured":"George C N, Scott M, Shree P, et al. CIL: intermediate language and tools for analysis and transformation of C programs. In: Proceedings of the 11th International Conference on Compiler Construction. London: Springer, 2002. 213\u2013228"},{"key":"9039_CR19","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke E, Kroening D, Lerda F. A tool for checking ANSI-C programings. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2004. 168\u2013176"},{"key":"9039_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1455229.1455239","volume":"14","author":"Z J Yang","year":"2009","unstructured":"Yang Z J, Wang C, Gupta A, et al. Model checking sequential software programs via mixed symbolic analysis. ACM Trans Design Autom Electron Syst, 2009, 14: 1\u201326","journal-title":"ACM Trans Design Autom Electron Syst"},{"key":"9039_CR21","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"B Armin","year":"2003","unstructured":"Armin B, Clarke E M, Zhu Y S. Bounded model checking. Adv Comput, 2003, 58: 117\u2013148","journal-title":"Adv Comput"},{"key":"9039_CR22","first-page":"202","volume-title":"Proceedings of the 35th International Conference on Software Engineering","author":"C Tian","year":"2013","unstructured":"Tian C, Duan Z H. Detecting spurious counterexamples efficiently in abstract model checking. In: Proceedings of the 35th International Conference on Software Engineering, San Francisco, 2013. 202\u2013211"},{"key":"9039_CR23","doi-asserted-by":"crossref","first-page":"1206","DOI":"10.1109\/TSE.2014.2357442","volume":"40","author":"C Tian","year":"2014","unstructured":"Tian C, Duan Z H, Duan Z. Making CEGAR more efficient in software model checking. IEEE Trans Softw Eng, 2014, 40: 1206\u20131223","journal-title":"IEEE Trans Softw Eng"},{"key":"9039_CR24","doi-asserted-by":"crossref","first-page":"1278","DOI":"10.1109\/TSE.1987.232881","volume":"13","author":"V R Basili","year":"1987","unstructured":"Basili V R, Selby R W. Comparing the effectiveness of software testing strategies. IEEE Trans Softw Eng, 1987, 13: 1278\u20131296","journal-title":"IEEE Trans Softw Eng"},{"key":"9039_CR25","doi-asserted-by":"crossref","first-page":"1844","DOI":"10.1145\/2480362.2480706","volume-title":"Proceedings of the 28th Annual ACM Symposium on Applied Computing","author":"J Hoffmann","year":"2013","unstructured":"Hoffmann J, Ussath M, Holz T, et al. Slicing droids: program slicing for smali code. In: Proceedings of the 28th Annual ACM Symposium on Applied Computing, Portugal, 2013. 1844\u20131851"},{"key":"9039_CR26","first-page":"274","volume-title":"Proceedings of the 18th Asia-Pacific Software Engineering Conference","author":"J Chen","year":"2011","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, Washington, 2011. 274\u2013281"},{"key":"9039_CR27","first-page":"200","volume-title":"Proceedings of the IEEE 22nd International Symposium on Software Reliability Engineering","author":"Y J Choi","year":"2011","unstructured":"Choi Y J. Safety analysis of trampoline OS using model checking: an experience report. In: Proceedings of the IEEE 22nd International Symposium on Software Reliability Engineering, Washington, 2011. 200\u2013209"},{"key":"9039_CR28","first-page":"142","volume-title":"Proceedings of the 5th International Symposium on Theoretical Aspects of Software Engineering","author":"Y H Huang","year":"2011","unstructured":"Huang Y H, Zhao Y X, Zhu L F, et al. Modeling and verifying the code-level OSEK\/VDX operating system with CSP. In: Proceedings of the 5th International Symposium on Theoretical Aspects of Software Engineering, Xi\u2019an, 2011. 142\u2013149"},{"key":"9039_CR29","first-page":"307","volume-title":"Proceedings of the 20th Asia-Pacific Software Engineering Conference","author":"H T Zhang","year":"2013","unstructured":"Zhang H T, Aoki T, Lin X H, et al. SMT-based bounded model checking for OSEK\/VDX applications. In: Proceedings of the 20th Asia-Pacific Software Engineering Conference, Bangkok, 2013. 307\u2013314"},{"key":"9039_CR30","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1145\/314602.314605","volume":"21","author":"Z M Liu","year":"1999","unstructured":"Liu Z M, Joseph M. Specification and verification of fault-tolerance, timing, and scheduling. ACM Trans Program Lang Syst, 1999, 21: 46\u201389","journal-title":"ACM Trans Program Lang Syst"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-016-9039-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-016-9039-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-016-9039-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,15]],"date-time":"2020-10-15T10:14:33Z","timestamp":1602756873000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-016-9039-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,11]]},"references-count":30,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,5]]}},"alternative-id":["9039"],"URL":"https:\/\/doi.org\/10.1007\/s11432-016-9039-4","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,11]]},"article-number":"052102"}}