Skip to main content
SpringerLink
Log in

Relational Concurrent Refinement

  • Chapter
  • First Online:
Book cover Refinement

  • 297 Accesses

Abstract

In the previous parts of the book, basic refinement relations were introduced semantically and for a variety of specification languages. This chapter starts the task of relating these different refinement relations by defining corresponding processes for ADT specifications, as well as process semantics for ADT specifications, and providing theorems relating refinement relations across formalisms via such embeddings.

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
Hardcover Book
USD 54.99
Price excludes VAT (USA)
  • Durable hardcover 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.

    See [1].

  2. 2.

    This condition is left implicit in the rest of this chapter.

References

  1. Derrick J, Boiten EA (2003) Relational concurrent refinement. Form Asp Comput 15(1):182–214

    Article  Google Scholar 

  2. Schneider S (2006) Non-blocking data refinement and traces-divergences semantics, personal communication

    Google Scholar 

  3. Bolton C, Davies J (2002) Refinement in Object-Z and CSP. In: Butler M, Petre L, Sere K (eds) Integrated formal methods (IFM 2002). Lecture notes in computer science, vol 2335. Springer, Berlin, pp 225–244

    Google Scholar 

  4. Bolton C, Davies J (2006) A singleton failures semantics for communicating sequential processes. Form Asp Comput 18(2):181–210

    Article  Google Scholar 

  5. Josephs MB (1988) A state-based approach to communicating processes. Distrib Comput 3:9–18

    Article  Google Scholar 

  6. Boiten EA, Derrick J (2002) Unifying concurrent and relational refinement. In: Derrick J, Boiten EA, von Wright J, Woodcock JCP (eds) ENTCS. Proceedings REFINE’02, vol 70

    Google Scholar 

  7. Reeves S, Streader D (2008) Data refinement and singleton failures refinement are not equivalent. Form Asp Comput 20(3):295–301

    Article  Google Scholar 

  8. Boiten EA, Derrick J, Schellhorn G (2009) Relational concurrent refinement II: internal operations and outputs. Form Asp Comput 21(1–2):65–102

    Article  Google Scholar 

  9. Derrick J, Boiten EA (2008) More relational refinement: traces and partial relations. Electron Notes Theor Comput Sci 214:255–276 (Proceedings of REFINE, Turku, 2008)

    Google Scholar 

  10. Boiten EA, Derrick J (2009) Modelling divergence in relational concurrent refinement. In: Leuschel M, Wehrheim H (eds) IFM 2009: Integrated formal methods. Lecture notes in computer science, vol 5423. Springer, Berlin, pp 183–199

    Google Scholar 

  11. Bolton C (2002) On the refinement of state-based and event-based models. PhD thesis, University of Oxford

    Google Scholar 

  12. van Glabbeek RJ (2001) The linear time - branching time spectrum I. The semantics of concrete sequential processes. In: Bergstra JA, Ponse A, Smolka SA (eds) Handbook of process algebra. Amsterdam, North-Holland, pp 3–99

    Google Scholar 

  13. Bolton C, Lowe G (2005) A hierarchy of failures-based models: theory and application. Theor Comput Sci 330(3):407–438

    Article  MathSciNet  Google Scholar 

  14. Bolton C, Lowe G (2003) A hierarchy of failures-based models. In: Corradini F, Westmann U (eds) Proceedings of express 2003: 10th international workshop on expressiveness in concurrency. Elsevier Science Publishers, Amsterdam

    Google Scholar 

  15. Reeves S, Streader D (2006) State- and event-based refinement. Technical report, University of Waikato, Department of computer science, University of Waikato, New Zealand

    Google Scholar 

  16. Lynch N, Tuttle M (1989) An introduction to input/output automata. CWI Q 2(3):219–246

    MathSciNet  MATH  Google Scholar 

  17. Tretmans J (1996) Test generation with inputs, outputs, and quiescence. In: Margaria T, Steffen B (eds) Second international workshop on tools and algorithms for the construction and analysis of systems (TACAS’96). Lecture notes in computer science, vol 1055. Springer, Berlin, pp 127–146

    Google Scholar 

  18. Lynch N, Vaandrager FW (1995) Forward and backward simulations I: untimed systems. Inf Comput 121(2):214–233

    Article  MathSciNet  Google Scholar 

  19. Segala R (1997) Quiescence, fairness, testing, and the notion of implementation. Inf Comput 138(2):194–210

    Article  MathSciNet  Google Scholar 

  20. Segala R (1993) Quiescence, fairness, testing, and the notion of implementation (extended abstract). In: International conference on concurrency theory, pp 324–338

    Google Scholar 

  21. Vaandrager FW (1991) On the relationship between process algebra and input/output automata. Logic in computer science, pp 387–398

    Google Scholar 

  22. de Nicola R, Segala R (1995) A process algebraic view of I/O automata. Theor Comput Sci 138:391–423

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Sheffield, Sheffield, UK

    John Derrick

  2. School of Computer Science and Informatics, De Montfort University, Leicester, Leicestershire, UK

    Eerke Boiten

Authors
  1. John Derrick
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eerke Boiten
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to John Derrick .

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Derrick, J., Boiten, E. (2018). Relational Concurrent Refinement. In: Refinement. Springer, Cham. https://doi.org/10.1007/978-3-319-92711-4_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-92711-4_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-92709-1

  • Online ISBN: 978-3-319-92711-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation