iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/S10703-006-0029-7
An abstract interpretation toolkit for μCRL | Formal Methods in System Design Skip to main content
Springer Nature Link
Log in

An abstract interpretation toolkit for μCRL

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

This paper describes a toolkit that assists in the task of generating abstract approximations of process algebraic specifications written in the language μCRL. Abstractions are represented by Modal Labelled Transition Systems, which are mixed transition systems with may and must modalities. The approach permits to infer the satisfaction or refutation of safety and liveness properties expressed in the (action-based) μ-calculus. The tool supports the abstraction of states and action labels, which allows to deal with infinitely branching systems.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Ball T, Majumdar R, Millstein T, Rajamani SK (2001) Automatic predicate abstraction of C programs. In: Proceedings of Conference on Programming Language Design and Implementation (PLDI), ACM, pp 203–213

  2. Ball T, Rajamani SK (2000) BeBop: a symbolic model checker for Boolean programs. In: Proceedings of SPIN model checking and software verification, LNCS, vol 1885, Springer, pp 113–130

  3. Ball T, Rajamani SK (2001) Automatically validating temporal safety properties of interfaces. In: Proceedings of SPIN model checking and software verification, LNCS, vol 2057. Springer, pp 103–122

  4. Bergstra JA, Klop JW (1985) Algebra of communicating processes with abstraction. Theor Comput Sci 37:77–121

    Article  MATH  Google Scholar 

  5. Blom S, Fokkink W, Groote JF, van Langevelde I, Lisser B, van de Pol JC (2001) μCRL: a toolset for analysing algebraic specifications. In: Proceedings of Computer Aided Verification (CAV), LNCS, vol 2102. Springer, pp 250–254

  6. Blom S, Groote JF, van Langevelde I, Lisser B, van de Pol JC (2003) New developments around the μCRL tool set. ENTCS 80

  7. Bruns G, Godefroid P (1999) Model checking partial state spaces with 3-valued temporal logics. In: Proceedings of Computer Aided Verification (CAV), LNCS, vol 1877. Springer, pp 274–287

  8. Clarke EM, Grumberg O, Long DE (1992) Model checking and abstraction. J ACM, pp 343–354

  9. Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixed points. J ACM 238–252

  10. Dams D (1996) Abstract interpretation and partition refinement for model checking. PhD thesis, Eindhoven University of Technology

  11. Dams D (2002) Abstraction in software model checking: principles and practice (tutorial overview and bibliography). In: Proceedings of SPIN model checking and software verification, LNCS, vol 2318, Springer, pp 14–21

  12. Dams D, Gerth R (2000) The bounded retransmission protocol revisited. ENTCS 9

  13. Dams D, Hesse W, Holzmann G (2002) Abstracting C with abC. In: Proceedings of the Computer Aided Verification (CAV), LNCS, vol 2404, Springer, pp 515–520

  14. Long DE (1993) Model checking, abstraction, and compositional verification. PhD thesis, Carnegie Mellon University

  15. Gallardo MM, Martínez J, Merino P, Pimentel E (2004) αSPIN: a tool for abstract model checking. Int J Softw Tools for Technol Transf (STTT) 5(2–3):165–184

    Google Scholar 

  16. Garavel H, Lang F, Mateescu R (2002) An overview of CADP 2001. Eur Assoc Softw Sci Technol Newsl 4:13–24

    Google Scholar 

  17. Godefroid P, Huth M, Jagadeesan R (2001) Abstraction-based model checking using modal transition systems. In: Proceedings of the concurrency theory (CONCUR), LNCS, vol 2154, Springer, pp 426–440

  18. Groote JF, van de Pol JC (1996) A bounded retransmission protocol for large data packets. In: Proceedings of the Algebraic Methodology and Software Technology (AMAST), LNCS, vol 1101. Springer, pp 536–550

  19. Groote JF, Ponse A (1994) The syntax and semantics of μCRL. In: Algebra of communicating processes, workshops in computing. pp 26–62

  20. Groote JF, Ponse A, Usenko Y (2001) Linearization in parallel pCRL. J Logic Algebraic Programm 48(1–2):39–70

    Article  MATH  Google Scholar 

  21. Hatcliff J, Dwyer M, Pasareanu C, Robby (2002) Foundations of the Bandera abstraction tools. In: Proceedings of the essence of computation, LNCS, vol 2566, Springer, pp 172–203

  22. Havelund K, Skakkebaek J (1999) Applying model checking in Java verification. In: Proceedings of the SPIN model checking and software verification, LNCS, vol 1680, Springer, pp 216–232

  23. Holzmann GJ, Smith MH (1999) A practical method for verifying event-driven software. In: Proceedings of International Conference on Software Engineering (ICSE). ACM, pp 597–607

  24. Huth M, Jagadeesan R, Schmidt D (2001) Modal transition systems: a foundation for three-valued program analysis. In: Proceedings of the programming languages and systems (ESOP), LNCS, vol 2028, Springer, pp 155–169

  25. Jones ND, Nielson F (1995) Abstract interpretation: a semantics-based tool for program analysis. In: Handbook of logic in computer science. Oxford Science Publications, pp 527–636

  26. Kozen D (1982) Results on the propositional μ-calculus. In: Proceedings of the International Conference on Automata, Languages and Programming (ICALP), LNCS, vol 140. Springer, pp 348–359

  27. Kroening D, Groce A, Clarke EM (2004) Counterexample guided abstraction refinement via program execution. In: Proceedings of the international conference on formal engineering methods (ICFEM), LNCS, vol 3380. Springer, pp 224–238

  28. Larsen KG, Thomsen B (1988) A modal process logic. In: Proceedings of the logic in computer science (LICS). IEEE, pp 203–210

  29. Manna Z, Colon M, Finkbeiner B, Sipma H, Uribe TE (1997) Abstraction and modular verification of infinite-state reactive systems. In: Proceedings of the requirements targeting software and systems engineering (RTSE), LNCS, vol 1526. Springer, pp 273–292

  30. Mateescu R (1998) Verification des proprietes temporelles des programmes paralleles. PhD thesis, Institut National Polytechnique de Grenoble

  31. Ore O (1944) Galois connexions. Trans. Am Math Soc 55:493–513

    Article  MATH  Google Scholar 

  32. Orzan S, van de Pol JC, Valero Espada M (2005) A state space distribution policy based on abstract interpretation. ENTCS 128:35–45

    Google Scholar 

  33. van de Pol JC (2001) A prover for the μCRL toolset with applications. Technical Report SEN-R0106, CWI

  34. van de Pol JC, Valero Espada M (2004) Modal abstraction in μCRL. In: Proceedings of the Algebraic Methodology and Software Technology (AMAST), LNCS, vol 3116, Springer, pp 409–425

  35. Schmidt D (2002) Structure-preserving binary relations for program abstraction. In: Proceedings of the essence of computation, LNCS, vol 2566, Springer, pp 245–268

  36. Usenko Y (2002) Linearization in μCRL. PhD thesis, Eindhoven University of Technology

  37. Valero M (2005) Modal abstraction and replication of processes with data. PhD thesis, Free University Amsterdam

  38. Willemse T (2003) Semantics and verification in process algebras with data and timing. PhD thesis, Eindhoven University of Technology

Download references

Author information

Authors and Affiliations

  1. Dept. de Sistemas Informáticos y Programación, Universidad Complutense de Madrid, E-28040, Madrid, Spain

    Miguel Valero Espada

  2. Centrum voor Wiskunde en Informatica, P.O.Box 94079, 1090, GB, Amsterdam, The Netherlands

    Jaco van de Pol

Authors
  1. Miguel Valero Espada
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jaco van de Pol
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Miguel Valero Espada.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Espada, M.V., Pol, J.v.d. An abstract interpretation toolkit for μCRL. Form Method Syst Des 30, 249–273 (2007). https://doi.org/10.1007/s10703-006-0029-7

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-006-0029-7

Keywords

Search

Navigation