{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T13:19:45Z","timestamp":1765545585317},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642103728"},{"type":"electronic","value":"9783642103735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_30","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T06:45:27Z","timestamp":1258353927000},"page":"581-600","source":"Crossref","is-referenced-by-count":17,"title":["Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction"],"prefix":"10.1007","author":[{"given":"Jun","family":"Sun","sequence":"first","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]},{"given":"Xian","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_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, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"30_CR2","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":"30_CR3","series-title":"Lecture Notes in Computer Science","first-page":"87","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.) Lectures on Concurrency and Petri Nets. LNCS, vol.\u00a03098, pp. 87\u2013124. Springer, Heidelberg (2004)"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"1998","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A Model-Checking Tool for Real-Time Systems. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 546\u2013550. Springer, Heidelberg (1998)"},{"key":"30_CR5","unstructured":"Brooke, P.: A Timed Semantics for a Hierarchical Design Notation. PhD thesis, University of York (1999)"},{"key":"30_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/3-540-44585-4_39","volume-title":"Computer Aided Verification","author":"E. Closse","year":"2001","unstructured":"Closse, E., Poize, M., Pulou, J., Sifakis, J., Venter, P., Weil, D., Yovine, S.: TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 391\u2013395. Springer, Heidelberg (2001)"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"6","key":"30_CR9","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1109\/TSE.2008.52","volume":"34","author":"J.S. Dong","year":"2008","unstructured":"Dong, J.S., Hao, P., Qin, S.C., Sun, J., Yi, W.: Timed Automata Patterns. IEEE Trans. Software Eng.\u00a034(6), 844\u2013859 (2008)","journal-title":"IEEE Trans. Software Eng."},{"key":"30_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11901433_19","volume-title":"Formal Methods and Software Engineering","author":"J.S. Dong","year":"2006","unstructured":"Dong, J.S., Hao, P., Sun, J., Zhang, X.: A Reasoning Method for Timed CSP Based on Constraint Solving. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 342\u2013359. Springer, Heidelberg (2006)"},{"key":"30_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1855","DOI":"10.1007\/3-540-48118-4_49","volume-title":"FM\u201999 - Formal Methods","author":"J.S. Dong","year":"1999","unstructured":"Dong, J.S., Mahony, B.P., Fulton, N.: Modeling Aircraft Mission Computer Task Rates. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol.\u00a01709, p. 1855. Springer, Heidelberg (1999)"},{"issue":"6","key":"30_CR12","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1145\/367766.368168","volume":"5","author":"R.W. Floyd","year":"1962","unstructured":"Floyd, R.W.: Algorithm 97: Shortest Path. Commun. ACM\u00a05(6), 345 (1962)","journal-title":"Commun. ACM"},{"key":"30_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/3-540-63166-6_23","volume-title":"Computer Aided Verification","author":"D. Harel","year":"1997","unstructured":"Harel, D.: Some Thoughts on Statecharts, 13 Years Later. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 226\u2013231. Springer, Heidelberg (1997)"},{"key":"30_CR14","doi-asserted-by":"crossref","unstructured":"Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal Modeling and Analysis of an Audio\/video Protocol: an Industrial Case Study using UPPAAL. In: RTSS 1997, pp. 2\u201313 (1997)","DOI":"10.7146\/brics.v4i31.18957"},{"issue":"2","key":"30_CR15","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T.A. Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Model Checking for Real-Time Systems. Information and Computation\u00a0111(2), 193\u2013244 (1994)","journal-title":"Information and Computation"},{"key":"30_CR16","series-title":"International Series in Computer Science","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"30_CR17","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. Addison Wesley, Reading (2003)"},{"key":"30_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BFb0014714","volume-title":"Hybrid and Real-Time Systems","author":"L.M. Lai","year":"1997","unstructured":"Lai, L.M., Watson, P.: A Case Study in Timed CSP: The Railroad Crossing Problem. In: Maler, O. (ed.) HART 1997. LNCS, vol.\u00a01201, pp. 69\u201374. Springer, Heidelberg (1997)"},{"key":"30_CR19","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Mikucionis, M., Nielsen, B., Skou, A.: Testing Real-time Embedded Software using UPPAAL-TRON: an Industrial Case Study. In: EMSOFT 2005, pp. 299\u2013306 (2005)","DOI":"10.1145\/1086228.1086283"},{"issue":"1-2","key":"30_CR20","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Wang, Y.: Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"2","key":"30_CR21","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1006\/inco.1997.2623","volume":"134","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Yi, W.: Time-abstracted Bisimulation: Implicit Specifications and Decidability. Information and Computation\u00a0134(2), 75\u2013101 (1997)","journal-title":"Information and Computation"},{"issue":"3","key":"30_CR22","first-page":"353","volume":"3","author":"M. Lindahl","year":"2001","unstructured":"Lindahl, M., Pettersson, P., Wang, Y.: Formal Design and Analysis of a Gearbox Controller. STTT 2001\u00a03(3), 353\u2013368 (2001)","journal-title":"STTT 2001"},{"issue":"5","key":"30_CR23","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/BF01211907","volume":"8","author":"N.A. Lynch","year":"1996","unstructured":"Lynch, N.A., Vaandrager, F.W.: Action Transducers and Timed Automata. Formal Aspects of Computing\u00a08(5), 499\u2013538 (1996)","journal-title":"Formal Aspects of Computing"},{"issue":"1","key":"30_CR24","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1006\/inco.1994.1083","volume":"114","author":"X. Nicollin","year":"1994","unstructured":"Nicollin, X., Sifakis, J.: The Algebra of Timed Processes, ATP: Theory and Application. Information and Computation\u00a0114(1), 131\u2013178 (1994)","journal-title":"Information and Computation"},{"issue":"9","key":"30_CR25","doi-asserted-by":"publisher","first-page":"794","DOI":"10.1109\/32.159837","volume":"18","author":"X. Nicollin","year":"1992","unstructured":"Nicollin, X., Sifakis, J., Yovine, S.: Compiling Real-Time Specifications into Extended Automata. IEEE Trans. Software Eng.\u00a018(9), 794\u2013804 (1992)","journal-title":"IEEE Trans. Software Eng."},{"key":"30_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"314","DOI":"10.1007\/3-540-16761-7_81","volume-title":"Automata, Languages and Programming","author":"G.M. Reed","year":"1986","unstructured":"Reed, G.M., Roscoe, A.W.: A Timed Model for Communicating Sequential Processes. In: Kott, L. (ed.) ICALP 1986. LNCS, vol.\u00a0226, pp. 314\u2013323. Springer, Heidelberg (1986)"},{"issue":"2","key":"30_CR27","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s00165-005-0065-x","volume":"17","author":"A.W. Roscoe","year":"2005","unstructured":"Roscoe, A.W.: On the expressive power of csp refinement. Formal Asp. Comput.\u00a017(2), 93\u2013112 (2005)","journal-title":"Formal Asp. Comput."},{"key":"30_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/3-540-60630-0_7","volume-title":"TACAS 1995","author":"A.W. Roscoe","year":"1995","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking csp or how to check 10 $^{\\mbox{20}}$ dining philosophers for deadlock. In: TACAS 1995. LNCS, vol.\u00a01019, pp. 133\u2013152. Springer, Heidelberg (1995)"},{"issue":"2","key":"30_CR29","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1995.1014","volume":"116","author":"S. Schneider","year":"1995","unstructured":"Schneider, S.: An Operational Semantics for Timed CSP. Information and Computation\u00a0116(2), 193\u2013213 (1995)","journal-title":"Information and Computation"},{"key":"30_CR30","volume-title":"Concurrent and Real-time Systems","author":"S. Schneider","year":"2000","unstructured":"Schneider, S.: Concurrent and Real-time Systems. John Wiley and Sons, Chichester (2000)"},{"key":"30_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/3-540-48683-6_2","volume-title":"Computer Aided Verification","author":"J. Sifakis","year":"1999","unstructured":"Sifakis, J.: The Compositional Specification of Timed Systems - A Tutorial. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 487\u2013490. Springer, Heidelberg (1999)"},{"key":"30_CR32","series-title":"CCIS","first-page":"307","volume-title":"ISOLA 2008","author":"J. Sun","year":"2008","unstructured":"Sun, J., Liu, Y., Dong, J.S.: Model Checking CSP Revisited: Introducing a Process Analysis Toolkit. In: Margaria, T., Steffen, B. (eds.) ISOLA 2008. CCIS, vol.\u00a017, pp. 307\u2013322. Springer, Heidelberg (2008)"},{"key":"30_CR33","series-title":"Lecture Notes in Computer Science","volume-title":"CAV 2009","author":"J. Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: CAV 2009. LNCS, vol.\u00a05643, Springer, Heidelberg (2009)"},{"key":"30_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"546","DOI":"10.1007\/3-540-61604-7_75","volume-title":"CONCUR \u201996: Concurrency Theory","author":"S. Tasiran","year":"1996","unstructured":"Tasiran, S., Alur, R., Kurshan, R.P., Brayton, R.K.: Verifying Abstractions of Timed Systems. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 546\u2013562. Springer, Heidelberg (1996)"},{"key":"30_CR35","first-page":"332","volume-title":"Proc. of the Symposium on Logic in Computer Science (LICS 1986)","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report). In: Proc. of the Symposium on Logic in Computer Science (LICS 1986), pp. 332\u2013344. IEEE Computer Society, Los Alamitos (1986)"},{"key":"30_CR36","unstructured":"Wang, F., Wu, R., Huang, G.: Verifying Timed and Linear Hybrid Rule-Systems with RED. In: SEKE 2005, pp. 448\u2013454 (2005)"},{"key":"30_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/3-540-54233-7_136","volume-title":"Automata, Languages and Programming","author":"W. Yi","year":"1991","unstructured":"Yi, W.: CCS + Time = An Interleaving Model for Real Time Systems. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 217\u2013228. Springer, Heidelberg (1991)"},{"key":"30_CR38","first-page":"243","volume-title":"FORTE 1994","author":"W. Yi","year":"1994","unstructured":"Yi, W., Pettersson, P., Daniels, M.: Automatic Verification of Real-time Communicating Systems by Constraint-Solving. In: FORTE 1994, pp. 243\u2013258. Chapman & Hall, Boca Raton (1994)"}],"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-10373-5_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:54:57Z","timestamp":1606168497000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}