Skip to main content
SpringerLink
Log in

CAAL: Concurrency Workbench, Aalborg Edition

  • Conference paper
  • First Online:
Theoretical Aspects of Computing - ICTAC 2015 (ICTAC 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9399))

Included in the following conference series:

Abstract

We present the first official release of Caal, a web-based tool for modelling and verification of concurrent processes. The tool is primarily designed for educational purposes and it supports the classical process algebra CCS together with its timed extension TCCS. It allows to compare processes with respect to a range of strong/weak and timed/untimed equivalences and preorders (bisimulation, simulation and traces) and supports model checking of CCS/TCCS processes against recursively defined formulae of Hennessy-Milner logic. The tool offers a graphical visualizer for displaying labelled transition systems, including their minimization up to strong/weak bisimulation, and process behaviour can be examined by playing (bi)simulation and model checking games or via the generation of distinguishing formulae for non-equivalent processes. We describe the modelling and analysis features of Caal, discuss the underlying verification algorithms and show a typical example of a use in the classroom environment.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In Caal dual channels are prefixed with an apostrophe and the output bar is displayed automatically by the editor.

References

  1. Aceto, L., Ingolfsdottir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling. Cambridge University Press, Specification and Verification (2007)

    Book  MATH  Google Scholar 

  2. Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Commun. ACM 12(5), 260–261 (1969)

    Article  Google Scholar 

  3. Birgisson, A.: CCS model checker in Haskell (2009). https://github.com/arnar/ccs-searching. Accessed on 03 August 2015

  4. Calzolai, F., De Nicola, R., Loreti, M., Tiezzi, F.: TAPAs: a tool for the analysis of process algebras. Trans. Petri Nets Other Models Concurr. 5100, 54–70 (2008)

    Article  MathSciNet  Google Scholar 

  5. Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. 15(1), 36–72 (1993)

    Article  Google Scholar 

  6. Cleaveland, R., Sims, S.: The NCSU concurrency workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 394–397. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  7. Freiberger, F., Biewer, S., Held, P.: PseuCo (2014). http://pseuco.com. Accessed on 03 August 2015

  8. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transfer 15(2), 89–107 (2013)

    Article  MATH  Google Scholar 

  9. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  10. Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. The MIT Press, Cambridge (2014)

    MATH  Google Scholar 

  11. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach. 32(1), 137–161 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  12. Kozen, D.: Results on the propositional \(\mu \)-calculus. Theoretical Computer Science 27, 333–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  13. Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, p. 53. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  14. Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Berlin (1980)

    MATH  Google Scholar 

  15. Mosegaard, M., Brabrand, C.: The bisimulation game (2006). http://www.brics.dk/bisim/. Accessed on 03 August 2015

  16. Verdejo, A., Marti-Oliet, N.: Executing and verifying CCS in Maude. Technical report, Dpto. Sistemas Informaticos y Programacion, Universidad Complutense de (2002). http://maude.cs.uiuc.edu/maude1/casestudies/ccs/

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Selma Lagerlöfs Vej 300, 9220, Aalborg Øst, Denmark

    Jesper R. Andersen, Nicklas Andersen, Søren Enevoldsen, Mathias M. Hansen, Kim G. Larsen, Simon R. Olesen, Jirí Srba & Jacob K. Wortmann

Authors
  1. Jesper R. Andersen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicklas Andersen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Søren Enevoldsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mathias M. Hansen
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Kim G. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Simon R. Olesen
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Jirí Srba
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. Jacob K. Wortmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jirí Srba .

Editor information

Editors and Affiliations

  1. University of Lübeck, Lübeck, Schleswig-Holstein, Germany

    Martin Leucker

  2. Pontificia Universidad Javeriana-Cali, Cali, Colombia

    Camilo Rueda

  3. Pontificia Universidad Javeriana-Cali, CNRS LIX École Polytechnique de Paris, Palaiseau Cedex, France

    Frank D. Valencia

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Andersen, J.R. et al. (2015). CAAL: Concurrency Workbench, Aalborg Edition. In: Leucker, M., Rueda, C., Valencia, F. (eds) Theoretical Aspects of Computing - ICTAC 2015. ICTAC 2015. Lecture Notes in Computer Science(), vol 9399. Springer, Cham. https://doi.org/10.1007/978-3-319-25150-9_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-25150-9_33

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-25149-3

  • Online ISBN: 978-3-319-25150-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation