Skip to main content
SpringerLink
Log in

Verifying Implementation Relations

  • Conference paper
  • First Online:
FME 2001: Formal Methods for Increasing Software Productivity (FME 2001)

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

Included in the following conference series:

Abstract

Implementation relations are a means to relate the behaviour of implementation and specification systems built of communicating processes in the event that respective implementation and specification processes have differing interfaces. In this paper we first present a graph-theoretic statement of such relations, and then derive algorithms for their automatic verification.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. J. Burton, M. Koutny and G. Pappalardo: Modelling and Verification of Communicating Processes in the Event of Interface Difference. Technical Report CS-TR-696, Department of Computing Science, University of Newcastle upon Tyne (2000).

    Google Scholar 

  2. P. Collette and C. B. Jones: Enhancing the Tractability of Rely/Guarantee Specifications in the Development of Interfering Operations. Technical Report CUMCS-95-10-3, Department of Computing Science, Manchester University (1995).

    Google Scholar 

  3. M. Hennessy: Algebraic Theory of Processes. MIT Press (1988).

    Google Scholar 

  4. C. A. R. Hoare: Communicating Sequential Processes. Prentice Hall (1985).

    Google Scholar 

  5. M. Koutny and G. Pappalardo: A Model of Behaviour Abstraction for Communicating Processes. Proc. of 16th Symposium on Theoretical Aspects of Computer Science, STACS’99, C. Meinel and S. Tison (Eds.). Springer-Verlag, Lecture Notes in Computer Science 1563 (1999) 313–322.

    Google Scholar 

  6. M. Koutny, L. Mancini and G. Pappalardo: Two Implementation Relations and the Correctness of Communicated Replicated Processing. Formal Aspects of Computing 9 (1997) 119–148.

    Article  MATH  Google Scholar 

  7. J. Burton and M. Koutny:Verification of Communicating Processes in the Event of Interface Difference. Proc. of International Workshop on Verification and Computational Logic, VCL2000,M. Leuschel, A. Podelski, C. Ramakrishnan and U. Ulrich-Nitsche (Eds.). Technical Report DSSE-TR-2000-6, University of Southampton (2000).

    Google Scholar 

  8. R. Milner: Communication and Concurrency. Prentice Hall (1989).

    Google Scholar 

  9. A. W. Roscoe: The Theory and Practice of Concurrency. Prentice-Hall (1998).

    Google Scholar 

  10. R. Sedgewick: Algorithms in C++. Addison-Wesley (1992).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Comp. Sci., University of Newcastle, Newcastle upon Tyne, NE1 7RU, UK

    Jonathan Burton & Maciej Koutny

  2. Dipartimento di Matematica e Informatica, Università degli Studi di Catania, Viale A. Doria 6, I-95125, Catania, Italy

    Giuseppe Pappalardo

Authors
  1. Jonathan Burton
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maciej Koutny
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Giuseppe Pappalardo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, University of Minho, Campus de Gualtar, 4700-320, Braga, Portugal

    José Nuno Oliveira

  2. AT&T Laboratories — Research, 180 Park Avenue, Florham Park, New Jersey, 07932, USA

    Pamela Zave

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Burton, J., Koutny, M., Pappalardo, G. (2001). Verifying Implementation Relations. In: Oliveira, J.N., Zave, P. (eds) FME 2001: Formal Methods for Increasing Software Productivity. FME 2001. Lecture Notes in Computer Science, vol 2021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45251-6_20

Download citation

  • DOI: https://doi.org/10.1007/3-540-45251-6_20

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41791-0

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation