{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:57:47Z","timestamp":1725569867841},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642169007"},{"type":"electronic","value":"9783642169014"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16901-4_37","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T17:40:06Z","timestamp":1289238006000},"page":"565-580","source":"Crossref","is-referenced-by-count":1,"title":["Making the Right Cut in Model Checking Data-Intensive Timed Systems"],"prefix":"10.1007","author":[{"given":"R\u00fcdiger","family":"Ehlers","sequence":"first","affiliation":[]},{"given":"Michael","family":"Gerke","sequence":"additional","affiliation":[]},{"given":"Hans-J\u00f6rg","family":"Peter","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"37_CR1","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. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"37_CR2","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"37_CR3","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":"37_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"1999","unstructured":"Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 341\u2013353. Springer, Heidelberg (1999)"},{"key":"37_CR5","unstructured":"Bengtsson, J.: Clocks, DBM, and States in Timed Systems. PhD thesis, Uppsala University (2002)"},{"key":"37_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-45251-6_18","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"D. Beyer","year":"2001","unstructured":"Beyer, D.: Improvements in BDD-based reachability analysis of timed automata. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 318\u2013343. Springer, Heidelberg (2001)"},{"key":"37_CR7","first-page":"317","volume-title":"ICCD","author":"S. Beyer","year":"2005","unstructured":"Beyer, S., B\u00f6hm, P., Gerke, M., Hillebrand, M.A., der Rieden, T.I., Knapp, S., Leinenbach, D., Paul, W.J.: Towards the formal verification of lower system layers in automotive systems. In: ICCD, pp. 317\u2013326. IEEE Computer Society, Los Alamitos (2005)"},{"issue":"4","key":"37_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R. Bloem","year":"2007","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from psl. Electr. Notes Theor. Comput. Sci.\u00a0190(4), 3\u201316 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"37_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-63166-6_19","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"1997","unstructured":"Bozga, M., Maler, O., Pnueli, A., Yovine, S.: Some progress in the symbolic verification of timed automata. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 179\u2013190. Springer, Heidelberg (1997)"},{"issue":"8","key":"37_CR10","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Computers"},{"issue":"2","key":"37_CR11","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput.\u00a098(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"issue":"4","key":"37_CR12","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model checker. STTT\u00a02(4), 410\u2013425 (2000)","journal-title":"STTT"},{"key":"37_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"key":"37_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-60045-0_66","volume-title":"Computer Aided Verification","author":"D.L. Dill","year":"1995","unstructured":"Dill, D.L., Wong-Toi, H.: Verification of real-time systems by successive over and under approximation. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 409\u2013422. Springer, Heidelberg (1995)"},{"key":"37_CR15","unstructured":"FlexRay Consortium: FlexRay Communications System Protocol Specification Version 2.1 Revision A (2005)"},{"key":"37_CR16","unstructured":"M\u00f8ller, J.B., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Fully symbolic model checking of timed systems using difference decision diagrams. Electr. Notes Theor. Comput. Sci.\u00a023(2) (1999)"},{"key":"37_CR17","first-page":"89","volume-title":"FMCAD","author":"F. Pigorsch","year":"2006","unstructured":"Pigorsch, F., Scholl, C., Disch, S.: Advanced unbounded model checking based on AIGs, BDD sweeping, and quantifier scheduling. In: FMCAD, pp. 89\u201396. IEEE Computer Society, Los Alamitos (2006)"},{"key":"37_CR18","unstructured":"Sentovich, E., Singh, K., Lavagno, L., Moon, C., Murgai, R., Saldanha, A., Savoj, H., Stephan, P., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: SIS: A system for sequential circuit synthesis. Technical Report UCB\/ERL M92\/41, EECS Department, University of California, Berkeley (1992)"},{"key":"37_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-45069-6_16","volume-title":"Computer Aided Verification","author":"S.A. Seshia","year":"2003","unstructured":"Seshia, S.A., Bryant, R.E.: Unbounded, fully symbolic model checking of timed automata using boolean methods. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 154\u2013166. Springer, Heidelberg (2003)"},{"key":"37_CR20","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram package release 2.4.2 (2009)"},{"issue":"1","key":"37_CR21","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10009-003-0135-4","volume":"6","author":"F. Wang","year":"2004","unstructured":"Wang, F.: Efficient verification of timed automata with BDD-like data structures. STTT\u00a06(1), 77\u201397 (2004)","journal-title":"STTT"},{"issue":"10","key":"37_CR22","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1002\/scj.10565","volume":"35","author":"S. Yamane","year":"2004","unstructured":"Yamane, S., Nakamura, K.: Development and evaluation of symbolic model checker based on approximation for real-time systems. Systems and Computers in Japan\u00a035(10), 83\u2013101 (2004)","journal-title":"Systems and Computers in Japan"},{"issue":"1-2","key":"37_CR23","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S.: Kronos: A verification tool for real-time systems. STTT\u00a01(1-2), 123\u2013133 (1997)","journal-title":"STTT"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16901-4_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T03:28:00Z","timestamp":1553225280000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}