Abstract
Specifying budgets and deadlines using a process algebra like CSP requires an explicit notion of time. The tock-CSP encoding embeds a rich and flexible approach for modelling discrete-time behaviours with powerful tool support. It uses an event tock, 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 tock-CSP, including specific operators, but the standard semantics remains inadequate. In this paper, we characterise tock-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 tock-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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Change history
15 October 2021
A Correction to this paper has been published: https://doi.org/10.1007/s00236-021-00409-7
References
Aceto, L., Murphy, D.: On the ill-timed but well-caused. In: Best, E. (ed.) CONCUR’93, pp. 97–111. Springer, Berlin (1993)
Andersen, H.R., Mendler, M.: An asynchronous process algebra with multiple clocks. In: Sannella, D. (ed.) Programming Languages and Systems—ESOP’94, pp. 58–73. Springer, Berlin (1994)
Armstrong, P., Lowe, G., Ouaknine, J., Roscoe, A.: Model checking Timed CSP. In: Proceedings of HOWARD (Festschrift for Howard Barringer) (2012)
Baeten, J.C.M., Bergstra, J.A.: Discrete time process algebra. Formal Aspects Comput. 8(2), 188–208 (1996)
Baxter, J., Ribeiro, P.: Tick-tock-CSP in Isabelle/HOL (2019). https://github.com/robo-star/tick-tock-CSP/
Berry, G., Cosserat, L.: The ESTEREL synchronous programming language and its mathematical semantics. In: International Conference on Concurrency, pp. 389–448. Springer, Berlin (1984)
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)
Chen, L.: An interleaving model for real-time systems. In: Nerode, A., Taitslin, M. (eds.) Logical Foundations of Computer Science—Tver’92, pp. 81–86. Springer, Berlin (1992)
Cleaveland, R., Hennessy, M.: Priorities in process algebras. Inf. Comput. 87(1), 58–77 (1990). https://doi.org/10.1016/0890-5401(90)90059-Q. Special Issue: Selections from 1988 IEEE Symposium on Logic in Computer Science
Davies, J.: Specification and Proof in Real Time CSP, vol. 6. Cambridge University Press, Cambridge (1993)
Evans, N., Schneider, S.: Analysing time dependent security properties in CSP using PVS. In: European Symposium on Research in Computer Security, pp. 222–237. Springer, Berlin (2000)
Gerth, R., Boucher, A.: A timed failures model for extended communicating processes. In: Ottmann, T. (ed.) Automata, Languages and Programming, pp. 95–114. Springer, Berlin (1987)
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: FDR3—A Modern Refinement Checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS, Lecture Notes in Computer Science, vol. 8413, pp. 187–201 (2014)
Göthel, 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–12. Springer, Cham (2015)
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–274 (1990)
Hennessy, M., Regan, T.: A process algebra for timed systems. Inf. Comput. 117(2), 221–239 (1995)
Isobe, Y., Moller, F., Nguyen, H.N., Roggenbach, M.: Safety and line capacity in railways—an approach in Timed CSP. In: International Conference on Integrated Formal Methods, pp. 54–68. Springer, London (2012)
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–123. Springer, Berlin (2005)
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–351. Springer, Berlin (2011)
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–352. Springer, Berlin (1992)
Leuschel, M., Butler, M.: ProB: a model checker for B. In: International Symposium of Formal Methods Europe, pp. 855–874. Springer, Berlin (2003)
Lowe, G., Ouaknine, J.: On timed models and full abstraction. Electron. Notes Theor. Comput. Sci. 155, 497–519 (2006)
Mestel, D., Roscoe, A.: Reducing complex CSP models to traces via priority. Electron. Notes Theor. Comput. Sci. 325, 237–252 (2016)
Mestel, D., Roscoe, A.W.: Translating between models of concurrency. Acta Inf. 57(3), 403–438 (2020)
Milner, R.: A Calculus of Communicating Systems. Springer, Berlin (1982)
Milner, R.: Calculi for synchrony and asynchrony. Theoret. Comput. Sci. 25(3), 267–310 (1983)
Moller, F., Tofts, C.: A temporal calculus of communicating systems. In: International Conference on Concurrency Theory, pp. 401–415. Springer, Berlin (1990)
Mukarram, A.: A refusal testing model for CSP. Ph.D. Thesis, University of Oxford (1993)
Nicollin, X., Sifakis, J.: The algebra of timed processes, ATP: theory and application. Inf. Comput. 114(1), 131–178 (1994)
Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002)
Ouaknine, J.: Discrete analysis of continuous behaviour in real-time concurrent systems. Ph.D. Thesis, University of Oxford (2000)
Ouaknine, J., Worrell, J.: Timed CSP = closed timed automata. Electron. Notes Theor. Comput. Sci. 68(2), 142–159 (2002)
Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: International Conference on Automated Deduction, pp. 748–752. Springer, Berlin (1992)
Phillips, I.: Refusal testing. Theoret. Comput. Sci. 50(3), 241–284 (1987)
Roscoe, A.: The expressiveness of CSP with priority. Electron. Notes Theor. Comput. Sci. 319, 387–401 (2015)
Roscoe, A., Reed, G.: A timed model for communicating sequential processes. Theoret. Comput. Sci. 58, (1988)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Upper Saddle River (1998)
Roscoe, A.W.: Understanding Concurrent Systems. Springer, Berlin (2010)
Roscoe, A.W.: The automated verification of timewise refinement. In: First Open EIT ICT Labs Workshop on Cyber-Physical Systems Engineering (2013)
Schneider, S.: Concurrent and Real-Time Systems. Wiley, London (2000)
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–July 2, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5643, pp. 709–714. Springer, Berlin (2009)
Woodcock, J.C.P., Davies, J.: Using Z-Specification, Refinement, and Proof. Prentice-Hall, Upper Saddle River (1996)
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–228. Springer, Berlin (1991)
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
The original online version of this article was revised due to error in text.
This work is funded by EPSRC Grants EP/M025756/1 and EP/R025479/1, and by the Royal Academy of Engineering. No new primary data was created as part of the study reported here.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Baxter, J., Ribeiro, P. & Cavalcanti, A. Sound reasoning in tock-CSP. Acta Informatica 59, 125–162 (2022). https://doi.org/10.1007/s00236-020-00394-3
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00236-020-00394-3