Abstract
µCRL [13] is a language for specifying and verifying distributed systems in an algebraic fashion. It targets the specification of system behaviour in a process-algebraic style and of data elements in the form of abstract data types. The µCRL toolset [21] (see http://www.cwi.nl/~mcrl) supports the analysis and manipulation of µCRL specifications. A µCRL specification can be automatically transformed into a linear process operator (LPO). All other tools in the µCRL toolset use LPOs as their starting point. The simulator allows the interactive simulation of an LPO. There are a number of tools that allow optimisations on the level of LPOs. The instantiator generates a labelled transition system (LTS) from an LPO (under the condition that it is finite-state), and the resulting LTS can be visualised, analysed and minimised.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Th. Arts and I.A. van Langevelde. How µCRL supported a smart redesign of a real-world protocol. In Proc. FMICS’99, pp. 31–53, 1999.
Th. Arts and I.A. van Langevelde. Correct performance of transaction capabilities. In Proc. ICACSD’2001. IEEE, 2001.
M.A. Bezem and J.F. Groote. Invariants in process algebra with data. In Proc. 5th Conference on Concurrency Theory, LNCS 836, pp. 401–416. Springer, 1994.
S.C.C. Blom. Partial τ-confluence for efficient state space generation. Technical Report, CWI, 2001.
M.G.J. van den Brand, H. de Jong, P. Klint, and P.A. Olivier. Efficient annotated terms. Software-Practice and Experience, 30(3):259–291, 2000.
P.F.G. Dechering and I.A. van Langevelde. The verification of coordination. In Proc. COORDINATION’2000, LNCS 1906, pp. 335–340. Springer, 2000.
J.-C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, and M. Sighireanu. CADP-a protocol validation and verification toolbox. In Proc. 8th Conference on Computer-Aided Verification, LNCS 1102, pp. 437–440. Springer, 1996.
J.F. Groote and B. Lisser. Computer assisted manipulation of algebraic process specifications. Technical Report, CWI, 2001.
J.F. Groote, F. Monin, and J.C. van de Pol. Checking verifications of protocols and distributed systems by computer. In Proc. 9th Conference on Concurrency Theory, LNCS 1466, pp. 629–655. Springer, 1998.
J.F. Groote, J. Pang, and A.G. Wouters. Analysis of a distributed system for lifting trucks. Technical Report, CWI, 2001.
J.F. Groote and J.C. van de Pol. State space reduction using partial τ-confluence. In Proc. MFCS’2000, LNCS 1893, pp. 383–393. Springer, 2000.
J.F. Groote and J.C. van de Pol. Equational binary decision diagrams. In Proc. LPAR’2000, LNAI 1955, pp. 161–178. Springer, 2000.
J.F. Groote and A. Ponse. The syntax and semantics of µCRL. In Proc. ACP’94, Workshops in Computing, pp. 26–62. Springer, 1995.
J.F. Groote, A. Ponse, and Y.S. Usenko. Linearization of parallel pCRL. To appear in Journal of Logic and Algebraic Programming.
J.F. Groote and M.P.A. Sellink. Confluence for process verification. Theoretical Computer Science, 170(1/2):47–81, 1996.
J.F. Groote and J. Springintveld. Focus points and convergent process operators: a proof strategy for protocol verification. In Proc. ARTS’95, 1995.
I.A. van Langevelde. A compact file format for labeled transition systems. Technical Report SEN R0102, CWI, 2001.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
J.C. van de Pol. A prover for the µCRL toolset with applications — version 1. Technical Report SEN R0106, CWI, 2001.
Y.S. Usenko. State space generation for the HAVi leader election protocol. To appear in Science of Computer Programming.
A.G. Wouters. Manual for the µCRL toolset (version 1.11). Technical Report, CWI, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blom, S., Fokkink, W., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J. (2001). µCRL: A Toolset for Analysing Algebraic Specifications. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_23
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive