Skip to main content
SpringerLink
Log in

Modal Abstractions in μCRL

  • Conference paper
Algebraic Methodology and Software Technology (AMAST 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3116))

Abstract

We describe a framework to generate modal abstract approximations from process algebraic specifications, written in the language μCRL. We allow abstraction of state variables and action labels. Moreover, we introduce a new format for process specifications called Modal Linear Process Equation (MLPE). Every transition step may lead to a set of abstract tates labelled with a set of abstract actions. We use MLPEs to characterize abstract interpretations of systems and to generate Modal Labelled Transition Systems, in which transitions may have two modalities may and must. We prove that the abstractions are sound for the full action-based μ-calculus. Finally, we apply the result to check some safety and liveness properties for the bounded retransmission protocol.

Partially supported by PROGRESS, the embedded systems research program of the Dutch organisation for Scientific Research NWO, the Dutch Ministry of Economic Affairs and the Technology Foundation STW, grant CES.5009.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Blom, S., Fokkink, W.J., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.: μ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)

    Chapter  Google Scholar 

  2. Blom, S.C.C., Groote, J.F., van Langevelde, I.A., Lisser, B., van de Pol, J.C.: New developments around the μCRL tool set. In: ENTCS 80 (2003)

    Google Scholar 

  3. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: TOPLAS ACM, vol. 16, pp. 1512–1542 (1994)

    Google Scholar 

  4. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL ACM, pp. 238–252 (1977)

    Google Scholar 

  5. Dams, D.: Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology (1996)

    Google Scholar 

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

    Google Scholar 

  7. Fantechi, A., Gnesi, S., Latella, D.: Towards automatic temporal logic verification of value passing process algebra using abstract interpretation. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 562–578. Springer, Heidelberg (1996)

    Google Scholar 

  8. Fernandez, J.-C., Garavel, H., Kerbrat, A., Mounier, L., Mateescu, R., Sighireanu, M.: CADP – a protocol validation and verification toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 437–440. Springer, Heidelberg (1996)

    Google Scholar 

  9. Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  10. Groote, J.F., Ponse, A.: The syntax and semantics of μCRL. In: ACP, Workshops in Computing Series, pp. 26–62 (1995)

    Google Scholar 

  11. Groote, J.F., van de Pol, J.C.: A bounded retransmission protocol for large data packets. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 536–550. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  12. Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: a foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  13. Jones, N.D., Nielson, F.: Abstract interpretation: A semantics-based tool for program analysis. Handbook of Logic in Computer Science, 527–636 (1995)

    Google Scholar 

  14. Kozen, D.: Results on the propositional μ-calculus. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 348–359. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  15. Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE, Los Alamitos (1988)

    Google Scholar 

  16. Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design 6, 11–44 (1995)

    Google Scholar 

  17. Manna, Z., Colon, M., Finkbeiner, B., Sipma, H., Uribe, T.E.: Abstraction and modular verification of infinite-state reactive systems. In: Broy, M., Rumpe, B. (eds.) RTSE 1997. LNCS, vol. 1526, pp. 273–292. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  18. Owre, S., Rajan, S., Rushb, J.M., Shankar, N., Srivas, M.K.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411–414. Springer, Heidelberg (1996)

    Google Scholar 

  19. van de Pol, J.C., Valero Espada, M.: Modal abstraction in μCRL. Technical Report SEN-R0401, CWI (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Jaco van de Pol & Miguel Valero Espada

Authors
  1. Jaco van de Pol
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Miguel Valero Espada
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Stirling, FK9 4LA, Stirling, UK

    Charles Rattray

  2. University of Stirling, FK9 4LA, Stirling

    Savitri Maharaj

  3. Department of Computing Science and Mathematics, University of Stirling, FK9 4LA, Stirling, UK

    Carron Shankland

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

van de Pol, J., Valero Espada, M. (2004). Modal Abstractions in μCRL. In: Rattray, C., Maharaj, S., Shankland, C. (eds) Algebraic Methodology and Software Technology. AMAST 2004. Lecture Notes in Computer Science, vol 3116. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27815-3_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-27815-3_32

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22381-8

  • Online ISBN: 978-3-540-27815-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation