{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T05:17:37Z","timestamp":1740287857182,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540278825"},{"type":"electronic","value":"9783540317142"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11526841_31","type":"book-chapter","created":{"date-parts":[[2010,7,18]],"date-time":"2010-07-18T16:51:58Z","timestamp":1279471918000},"page":"465-480","source":"Crossref","is-referenced-by-count":10,"title":["Model-Checking of Specifications Integrating Processes, Data and Time"],"prefix":"10.1007","author":[{"given":"Jochen","family":"Hoenicke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Maier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0031985","volume-title":"Real-Time: Theory in Practice","author":"M. Abadi","year":"1992","unstructured":"Abadi, M., Lamport, L.: An old-fashioned recipe for real time. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol.\u00a0600, pp. 1\u201327. Springer, Heidelberg (1992)"},{"key":"31_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R. Alur","year":"1996","unstructured":"Alur, R., Henzinger, T.A., Ho, P.-H.: Automatic symbolic verification of embedded systems. IEEE Trans. Software Engineering\u00a022, 181\u2013201 (1996)","journal-title":"IEEE Trans. Software Engineering"},{"key":"31_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 260\u2013264. Springer, Heidelberg (2001)"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE 2003, pp. 385\u2013395 (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"31_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"G. Delzanno","year":"1999","unstructured":"Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 223\u2013239. Springer, Heidelberg (1999)"},{"key":"31_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/3-540-45739-9_25","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"H. Dierks","year":"2002","unstructured":"Dierks, H., Lettrari, M.: Constructing test automata from graphical real-time requirements. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 433\u2013454. Springer, Heidelberg (2002)"},{"key":"31_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-540-30482-1_39","volume-title":"Formal Methods and Software Engineering","author":"J.S. Dong","year":"2004","unstructured":"Dong, J.S., Hao, P., Qin, S.C., Sun, J., Yi, W.: Timed patterns: TCOZ to timed automata. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 483\u2013498. Springer, Heidelberg (2004)"},{"key":"31_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/3-540-45739-9_16","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"M. Fr\u00e4nzle","year":"2002","unstructured":"Fr\u00e4nzle, M.: Take it NP-easy: Bounded model construction for duration calculus. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 245\u2013264. Springer, Heidelberg (2002)"},{"key":"31_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"31_CR10","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"POPL 2002","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002, pp. 58\u201370. ACM Press, New York (2002)"},{"key":"31_CR11","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Hoenicke, J., Maier, P.: Model-checking of specifications integrating processes, data and time. Technical Report\u00a05, SFB\/TR 14 AVACS (2005), http:\/\/www.avacs.org\/","DOI":"10.1007\/11526841_31"},{"key":"31_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/3-540-47884-1_14","volume-title":"Integrated Formal Methods","author":"J. Hoenicke","year":"2002","unstructured":"Hoenicke, J., Olderog, E.-R.: Combining specification techniques for processes data and time. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol.\u00a02335, p. 245. Springer, Heidelberg (2002)"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Hoenicke, J., Olderog, E.-R.: CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nordic Journal of Computing\u00a09(4) (2002)","DOI":"10.1007\/3-540-47884-1_14"},{"key":"31_CR15","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM TOPLAS\u00a016, 872\u2013973 (1994)","journal-title":"ACM TOPLAS"},{"key":"31_CR16","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1145\/1040305.1040317","volume-title":"POPL 2005","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: POPL 2005, pp. 132\u2013144. ACM Press, New York (2005)"},{"key":"31_CR17","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1998","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"31_CR18","unstructured":"Rybalchenko, A.: A model checker based on abstraction refinement. Master\u2019s thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Saarland (September 2002)"},{"key":"31_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-540-31980-1_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Sharma","year":"2005","unstructured":"Sharma, B., Pandya, P.K., Chakraborty, S.: Bounded validity checking of interval duration logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 301\u2013316. Springer, Heidelberg (2005)"},{"key":"31_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/BFb0015015","volume-title":"CONCUR \u201994: Concurrency Theory","author":"J.U. Skakkeb\u00e6k","year":"1994","unstructured":"Skakkeb\u00e6k, J.U.: Liveness and fairness in duration calculus. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol.\u00a0836, pp. 283\u2013298. Springer, Heidelberg (1994)"},{"key":"31_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-5265-9","volume-title":"The Object-Z Specification Language","author":"G. Smith","year":"2000","unstructured":"Smith, G.: The Object-Z Specification Language. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"31_CR22","series-title":"Prentice-Hall International Series in Computer Science","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1992)","edition":"2"},{"key":"31_CR23","unstructured":"Tapken, J.: Model-Checking of Duration Calculus Specifications. PhD thesis, University of Oldenburg (June 2001)"},{"key":"31_CR24","doi-asserted-by":"crossref","unstructured":"Yovine, S.: Kronos: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer\u00a01(1+2) (1997)","DOI":"10.1007\/s100090050009"},{"key":"31_CR25","series-title":"EATCS: Monographs in Theoretical Computer Science","volume-title":"Duration Calculus: A Formal Approach to Real-Time Systems","author":"C. Zhou","year":"2004","unstructured":"Zhou, C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. EATCS: Monographs in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"issue":"5","key":"31_CR26","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"C. Zhou","year":"1991","unstructured":"Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters\u00a040(5), 269\u2013276 (1991)","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","FM 2005: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11526841_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T02:30:27Z","timestamp":1740277827000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11526841_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540278825","9783540317142"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11526841_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}