{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,28]],"date-time":"2026-03-28T04:29:03Z","timestamp":1774672143453,"version":"3.50.1"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,4,17]],"date-time":"2021-04-17T00:00:00Z","timestamp":1618617600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,4,17]],"date-time":"2021-04-17T00:00:00Z","timestamp":1618617600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/M025756\/1"],"award-info":[{"award-number":["EP\/M025756\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R025479\/1"],"award-info":[{"award-number":["EP\/R025479\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000287","name":"Royal Academy of Engineering","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000287","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2022,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Specifying budgets and deadlines using a process algebra like CSP requires an explicit notion of time. The <jats:italic>tock<\/jats:italic>-CSP encoding embeds a rich and flexible approach for modelling discrete-time behaviours with powerful tool support. It uses an event <jats:italic>tock<\/jats:italic>, interpreted to mark passage of time. Analysis, however, has traditionally used the standard semantics of CSP, which is inadequate for reasoning about timed refinement. The most recent version of the model checker FDR provides tailored support for <jats:italic>tock<\/jats:italic>-CSP, including specific operators, but the standard semantics remains inadequate. In this paper, we characterise <jats:italic>tock<\/jats:italic>-CSP as a language in its own right, rich enough to model budgets and deadlines, and reason about Zeno behaviour. We present the first sound tailored semantic model for <jats:italic>tock<\/jats:italic>-CSP that captures timewise refinement. It is fully mechanised in Isabelle\/HOL and, to enable use of FDR4 to check refinement in this novel model, we use model shifting, which is a technique that explicitly encodes refusals in traces.<\/jats:p>","DOI":"10.1007\/s00236-020-00394-3","type":"journal-article","created":{"date-parts":[[2021,4,17]],"date-time":"2021-04-17T02:03:05Z","timestamp":1618624985000},"page":"125-162","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Sound reasoning in tock-CSP"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6083-9607","authenticated-orcid":false,"given":"James","family":"Baxter","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4319-4872","authenticated-orcid":false,"given":"Pedro","family":"Ribeiro","sequence":"additional","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,4,17]]},"reference":[{"key":"394_CR1","first-page":"97","volume-title":"CONCUR\u201993","author":"L Aceto","year":"1993","unstructured":"Aceto, L., Murphy, D.: On the ill-timed but well-caused. In: Best, E. (ed.) CONCUR\u201993, pp. 97\u2013111. Springer, Berlin (1993)"},{"key":"394_CR2","first-page":"58","volume-title":"Programming Languages and Systems\u2014ESOP\u201994","author":"HR Andersen","year":"1994","unstructured":"Andersen, H.R., Mendler, M.: An asynchronous process algebra with multiple clocks. In: Sannella, D. (ed.) Programming Languages and Systems\u2014ESOP\u201994, pp. 58\u201373. Springer, Berlin (1994)"},{"key":"394_CR3","unstructured":"Armstrong, P., Lowe, G., Ouaknine, J., Roscoe, A.: Model checking Timed CSP. In: Proceedings of HOWARD (Festschrift for Howard Barringer) (2012)"},{"issue":"2","key":"394_CR4","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/BF01214556","volume":"8","author":"JCM Baeten","year":"1996","unstructured":"Baeten, J.C.M., Bergstra, J.A.: Discrete time process algebra. Formal Aspects Comput. 8(2), 188\u2013208 (1996)","journal-title":"Formal Aspects Comput."},{"key":"394_CR5","unstructured":"Baxter, J., Ribeiro, P.: Tick-tock-CSP in Isabelle\/HOL (2019). https:\/\/github.com\/robo-star\/tick-tock-CSP\/"},{"key":"394_CR6","doi-asserted-by":"crossref","unstructured":"Berry, G., Cosserat, L.: The ESTEREL synchronous programming language and its mathematical semantics. In: International Conference on Concurrency, pp. 389\u2013448. Springer, Berlin (1984)","DOI":"10.1007\/3-540-15670-4_19"},{"key":"394_CR7","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A., Sampaio, A., Miyazawa, A., Ribeiro, P., Conserva Filho, M., Didier, A., Li, W., Timmis, J.: Verified simulation for robotics. Sci. Comput. Program. (2019)","DOI":"10.1016\/j.scico.2019.01.004"},{"key":"394_CR8","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/BFb0023865","volume-title":"Logical Foundations of Computer Science\u2014Tver\u201992","author":"L Chen","year":"1992","unstructured":"Chen, L.: An interleaving model for real-time systems. In: Nerode, A., Taitslin, M. (eds.) Logical Foundations of Computer Science\u2014Tver\u201992, pp. 81\u201386. Springer, Berlin (1992)"},{"issue":"1","key":"394_CR9","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1016\/0890-5401(90)90059-Q","volume":"87","author":"R Cleaveland","year":"1990","unstructured":"Cleaveland, R., Hennessy, M.: Priorities in process algebras. Inf. Comput. 87(1), 58\u201377 (1990). https:\/\/doi.org\/10.1016\/0890-5401(90)90059-Q. Special Issue: Selections from 1988 IEEE Symposium on Logic in Computer Science","journal-title":"Inf. Comput."},{"key":"394_CR10","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569760","volume-title":"Specification and Proof in Real Time CSP","author":"J Davies","year":"1993","unstructured":"Davies, J.: Specification and Proof in Real Time CSP, vol. 6. Cambridge University Press, Cambridge (1993)"},{"key":"394_CR11","doi-asserted-by":"crossref","unstructured":"Evans, N., Schneider, S.: Analysing time dependent security properties in CSP using PVS. In: European Symposium on Research in Computer Security, pp. 222\u2013237. Springer, Berlin (2000)","DOI":"10.1007\/10722599_14"},{"key":"394_CR12","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/3-540-18088-5_9","volume-title":"Automata, Languages and Programming","author":"R Gerth","year":"1987","unstructured":"Gerth, R., Boucher, A.: A timed failures model for extended communicating processes. In: Ottmann, T. (ed.) Automata, Languages and Programming, pp. 95\u2013114. Springer, Berlin (1987)"},{"key":"394_CR13","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: FDR3\u2014A Modern Refinement Checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS, Lecture Notes in Computer Science, vol. 8413, pp. 187\u2013201 (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"394_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-15392-6_1","volume-title":"Nature of Computation and Communication","author":"T G\u00f6thel","year":"2015","unstructured":"G\u00f6thel, T., Bartels, B.: Modular design and verification of distributed adaptive real-time systems. In: Vinh, P.C., Vassev, E., Hinchey, M. (eds.) Nature of Computation and Communication, pp. 3\u201312. Springer, Cham (2015)"},{"key":"394_CR15","unstructured":"Groote, J.F.: Specification and verification of real time systems in ACP. In: Proceedings of the IFIP WG6.1 10th International Symposium on Protocol Specification, Testing and Verification X, pp. 261\u2013274 (1990)"},{"issue":"2","key":"394_CR16","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1006\/inco.1995.1041","volume":"117","author":"M Hennessy","year":"1995","unstructured":"Hennessy, M., Regan, T.: A process algebra for timed systems. Inf. Comput. 117(2), 221\u2013239 (1995)","journal-title":"Inf. Comput."},{"key":"394_CR17","doi-asserted-by":"crossref","unstructured":"Isobe, Y., Moller, F., Nguyen, H.N., Roggenbach, M.: Safety and line capacity in railways\u2014an approach in Timed CSP. In: International Conference on Integrated Formal Methods, pp. 54\u201368. Springer, London (2012)","DOI":"10.1007\/978-3-642-30729-4_5"},{"key":"394_CR18","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-31980-1_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Isobe","year":"2005","unstructured":"Isobe, Y., Roggenbach, M.: A generic theorem prover of CSP refinement. In: Halbwachs, N., Zuck, L.D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 108\u2013123. Springer, Berlin (2005)"},{"key":"394_CR19","doi-asserted-by":"crossref","unstructured":"Kharmeh, S.A., Eder, K., May, D.: A design-for-verification framework for a configurable performance-critical communication interface. In: International Conference on Formal Modeling and Analysis of Timed Systems, pp. 335\u2013351. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24310-3_23"},{"key":"394_CR20","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BFb0031999","volume-title":"Real-Time: Theory in Practice","author":"AS Klusener","year":"1992","unstructured":"Klusener, A.S.: Abstraction in real time process algebra. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) Real-Time: Theory in Practice, pp. 325\u2013352. Springer, Berlin (1992)"},{"key":"394_CR21","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: International Symposium of Formal Methods Europe, pp. 855\u2013874. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"394_CR22","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1016\/j.entcs.2005.11.070","volume":"155","author":"G Lowe","year":"2006","unstructured":"Lowe, G., Ouaknine, J.: On timed models and full abstraction. Electron. Notes Theor. Comput. Sci. 155, 497\u2013519 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"394_CR23","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/j.entcs.2016.09.041","volume":"325","author":"D Mestel","year":"2016","unstructured":"Mestel, D., Roscoe, A.: Reducing complex CSP models to traces via priority. Electron. Notes Theor. Comput. Sci. 325, 237\u2013252 (2016)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3","key":"394_CR24","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/s00236-020-00372-9","volume":"57","author":"D Mestel","year":"2020","unstructured":"Mestel, D., Roscoe, A.W.: Translating between models of concurrency. Acta Inf. 57(3), 403\u2013438 (2020)","journal-title":"Acta Inf."},{"key":"394_CR25","volume-title":"A Calculus of Communicating Systems","author":"R Milner","year":"1982","unstructured":"Milner, R.: A Calculus of Communicating Systems. Springer, Berlin (1982)"},{"issue":"3","key":"394_CR26","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R Milner","year":"1983","unstructured":"Milner, R.: Calculi for synchrony and asynchrony. Theoret. Comput. Sci. 25(3), 267\u2013310 (1983)","journal-title":"Theoret. Comput. Sci."},{"key":"394_CR27","doi-asserted-by":"crossref","unstructured":"Moller, F., Tofts, C.: A temporal calculus of communicating systems. In: International Conference on Concurrency Theory, pp. 401\u2013415. Springer, Berlin (1990)","DOI":"10.1007\/BFb0039073"},{"key":"394_CR28","unstructured":"Mukarram, A.: A refusal testing model for CSP. Ph.D. Thesis, University of Oxford (1993)"},{"issue":"1","key":"394_CR29","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. Inf. Comput. 114(1), 131\u2013178 (1994)","journal-title":"Inf. Comput."},{"key":"394_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002)"},{"key":"394_CR31","unstructured":"Ouaknine, J.: Discrete analysis of continuous behaviour in real-time concurrent systems. Ph.D. Thesis, University of Oxford (2000)"},{"issue":"2","key":"394_CR32","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/S1571-0661(05)80369-X","volume":"68","author":"J Ouaknine","year":"2002","unstructured":"Ouaknine, J., Worrell, J.: Timed CSP = closed timed automata. Electron. Notes Theor. Comput. Sci. 68(2), 142\u2013159 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"394_CR33","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: International Conference on Automated Deduction, pp. 748\u2013752. Springer, Berlin (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"issue":"3","key":"394_CR34","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0304-3975(87)90117-4","volume":"50","author":"I Phillips","year":"1987","unstructured":"Phillips, I.: Refusal testing. Theoret. Comput. Sci. 50(3), 241\u2013284 (1987)","journal-title":"Theoret. Comput. Sci."},{"key":"394_CR35","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1016\/j.entcs.2015.12.023","volume":"319","author":"A Roscoe","year":"2015","unstructured":"Roscoe, A.: The expressiveness of CSP with priority. Electron. Notes Theor. Comput. Sci. 319, 387\u2013401 (2015)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"394_CR36","doi-asserted-by":"crossref","unstructured":"Roscoe, A., Reed, G.: A timed model for communicating sequential processes. Theoret. Comput. Sci. 58, (1988)","DOI":"10.1016\/0304-3975(88)90030-8"},{"key":"394_CR37","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1998","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Upper Saddle River (1998)"},{"key":"394_CR38","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2010","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Springer, Berlin (2010)"},{"key":"394_CR39","unstructured":"Roscoe, A.W.: The automated verification of timewise refinement. In: First Open EIT ICT Labs Workshop on Cyber-Physical Systems Engineering (2013)"},{"key":"394_CR40","volume-title":"Concurrent and Real-Time Systems","author":"S Schneider","year":"2000","unstructured":"Schneider, S.: Concurrent and Real-Time Systems. Wiley, London (2000)"},{"key":"394_CR41","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26\u2013July 2, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5643, pp. 709\u2013714. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"394_CR42","volume-title":"Using Z-Specification, Refinement, and Proof","author":"JCP Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z-Specification, Refinement, and Proof. Prentice-Hall, Upper Saddle River (1996)"},{"key":"394_CR43","doi-asserted-by":"publisher","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: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) Automata, Languages and Programming, pp. 217\u2013228. Springer, Berlin (1991)"}],"updated-by":[{"DOI":"10.1007\/s00236-021-00409-7","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000}}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00394-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-020-00394-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00394-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,17]],"date-time":"2022-02-17T11:10:01Z","timestamp":1645096201000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-020-00394-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,17]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["394"],"URL":"https:\/\/doi.org\/10.1007\/s00236-020-00394-3","relation":{"correction":[{"id-type":"doi","id":"10.1007\/s00236-021-00409-7","asserted-by":"object"}]},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,4,17]]},"assertion":[{"value":"26 November 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 December 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 April 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 October 2021","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s00236-021-00409-7","URL":"https:\/\/doi.org\/10.1007\/s00236-021-00409-7","order":7,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}