Skip to main content
SpringerLink
Log in

A Framework for Automatic Construction of Abstract Promela Models

  • Conference paper
  • First Online:
Theoretical and Practical Aspects of SPIN Model Checking (SPIN 1999)

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

Included in the following conference series:

Abstract

One of the current trends in model checking for the verification of concurrent systems is to reduce the state space produced by the model, and one of the more promising ways to achieve this objective is to support some kind of automatic construction of more abstract models. This paper presents a proposal in this direction. The main contribution of the paper is the definition of a semantics framework which allows us to relate different models of the system, each one with a particular abstraction level. Automatic source-to-source transformation is supported by this formal basis. The method is applied to Promela models.

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. Barlett A., Scantlebury R. A., Wilkinson P. T.:A note on reliable full-duplex trans-mission over half-duplex lines. Communications of the ACM, 12 (5)(1969) 260–265

    Article  Google Scholar 

  2. Cousot P., Cousot R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. Conference Record of the 4th ACM Symposium on Principles of Programming Languages 1977

    Google Scholar 

  3. Clarke E. M., Emerson E. A., Sistla A. P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. on Programming Languages and Systems, 8 (2), 1986 244–263

    Article  MATH  Google Scholar 

  4. Clarke E. M., Grumberg O., Long D. E.: Model Checking and Abstraction.ACM Transaction on Languages and Systems, 16(5) (1994) 1512–1542

    Article  Google Scholar 

  5. Clarke E. M., Wing J. M.: Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, ACM 50TH Anniversary Issue Workshop on Strategic Directions in Computing Research, 28(4) (1996)626–643

    Google Scholar 

  6. Dams D., Gerth R., Grumberg O.:Abstract Interpretation of Reactive Systems. ACM Transactions on Programming Languages and Systems, 19(2) March (1997) 253–291

    Article  Google Scholar 

  7. Giacobazzi R., Debray S. K., Levi G.: A Generalized Semantics for Constraint Logic Programs. Proceedings of the International Conference on Fifth Generation Computer Systems (1992) 581–591

    Google Scholar 

  8. Gunter C., Mitchell J.: Strategic Directions in Software Engineering and Programming Languages. ACM Workshop on Strategic Directions in Computing Research, ACM Computing Surveys, 28(4)(1996) 727–737

    Google Scholar 

  9. Gallardo M. M., Merino P., Troya J. M.: Relating Abstract Interpretation with Logic Program Verification. Proceedings of the International Workshop on Verification, Model Cheking and Abstract Interpretation, Port Jefferson, USA, (1997)

    Google Scholar 

  10. Gallardo M. M., Merino P.: A Formal basis to Improve the Automatic Verification of Concurrent Systems. Technical Report LCC IT 99/10. Dpto. de Lenguajes y Ciencias de la Computacion. University of Malaga.(1999)

    Google Scholar 

  11. Holzmann G. J.: Design and Validation of Computer Protocols.Prentice-Hall, New Jersey (1991)

    Google Scholar 

  12. Holzmann G. J.: Designing Bug-Free Protocols with SPIN. Computer Communications, 20(2) (1997) 97–105

    Article  Google Scholar 

  13. Jones, N.D., S-ndergaard, H.: A Semantics-based framework for the abstract interpretation of Prolog. Abstract Interpretation of Declarative Languages. S. Abramsky and C. Hankin, Eds. Ellis Horwood, Chichester, UK. (1987) 123–142

    Google Scholar 

  14. Natarajan V., Holzmann G. J.: Outline for an Operational Semantics of Promela. The SPIN Verification Systems. DIMACS Series in Discrete Mathematics and Theoretical Computer Science. AMS Vol.32 (1997) 133–152

    Google Scholar 

  15. Vardi M., Wolper P.: An Automata-Theoretic Approach to Automatic Program Verification. Proc. of the Symp. on Logic in Computer Science, Cambridge (1986)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dpto. de Lenguajes y Ciencias de la Computacion, University of Malaga, 29071, Malaga, Spain

    Maria-del-Mar Gallardo & Pedro Merino

Authors
  1. Maria-del-Mar Gallardo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pedro Merino
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Electrical Engineering and Department of Mathematics and Computer Science, Eindhoven University of Technology, 5600, MB Eindhoven, The Netherlands

    Dennis Dams

  2. Intel Microprocessor Products Group, Strategic CAD Laboratories, 5200 NE Elam Young Parkway, JFT-104, Hillsboro, OR, 97124-6497, USA

    Rob Gerth

  3. Department of Electrical and Computer Engineering, University of Waterloo, Waterloo, Ontario, N2L 3G1, Canada

    Stefan Leue

  4. C.N.R.-Ist., CNUCE via Santa Maria 36, 56126, Pisa, Italy

    Mieke Massink

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gallardo, MdM., Merino, P. (1999). A Framework for Automatic Construction of Abstract Promela Models. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds) Theoretical and Practical Aspects of SPIN Model Checking. SPIN 1999. Lecture Notes in Computer Science, vol 1680. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48234-2_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-48234-2_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66499-4

  • Online ISBN: 978-3-540-48234-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation