Abstract
μCRL is a process algebraic language for specification and verification of distributed systems. μCRL allows to describe temporal properties of distributed systems but it has no explicit reference to time. In this work we propose a manner of introducing discrete time without extending the language. The semantics of discrete time we use makes it possible to reduce the time progress problem to the diagnostics of “no action is enabled” situations. The synchronous nature of the language facilitates the task. We show some experimental verification results obtained on a timed communication protocol.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R.: Timed Automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999)
Baeten, J.C.M., Bergstra, J.A.: Discrete time process algebra. Formal Aspects of Computing 8(2), 188–208 (1996)
Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing: Real Time and Discrete Time. In: Bergstra et al. [4]
Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier, Amsterdam (2001)
Blom, S.C.C., Fokkink, W.J., Groote, J.F., van Langevelde, I.A., Lisser, B., van de Pol, J.C.: μCRL: a toolset for analysing algebraic specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 250–254. Springer, Heidelberg (2001)
Bošnački, D., Dams, D.: Integrating real time into Spin: A prototype implementation. In: Budkowski, S., Cavalli, A., Najm, E. (eds.) Proceedings of Formal Description Techniques and Protocol Specification, Testing, and Verification. Kluwer Academic Publishers, Dordrecht (1998)
Bozga, M., Maler, O., Tripakis, S.: Efficient verification of timed automata using dense and disrete time semantics. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 125–141. Springer, Heidelberg (1999)
Groote, J.F., Reniers, M.: Algebraic process verification. In: Bergstra et al. [4], pp. 1151–1208
Groote, J.F., van Wamel, J.J.: Analysis of three hybrid systems in timed μCRL. Science of Computer Programming 39, 215–247 (2001)
Groote, J.F.: The syntax and semantics of timed μCRL. SEN R9709, CWI, Amsterdam (1997)
Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)
Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. In: Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000 (2000)
Nicola, R.D., Vaandrager, F.: Three logics for branching bisimulation. Journal of the ACM(JACM) 42(2), 458–487 (1996)
ObjectGeode 4 (2000), http://www.csverilog.com/products/geode.htm
Tanenbaum, A.S.: Computer Networks. Prentice Hall International, Inc., Englewood Cliffs (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blom, S., Ioustinova, N., Sidorova, N. (2004). Timed Verification with μCRL. In: Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 2003. Lecture Notes in Computer Science, vol 2890. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39866-0_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-39866-0_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20813-6
Online ISBN: 978-3-540-39866-0
eBook Packages: Springer Book Archive