Skip to main content
SpringerLink
Log in

Relating Data Refinement and Failures-Divergences Refinement

  • Chapter
  • First Online:
Refinement

  • 299 Accesses

Abstract

Chapter  9 discussed the general approach to relating process refinement and relational refinement by developing a relational framework general enough that we could embed some of the refinement relations we discussed in Chap. 1. This included a brief discussion of the simulation rules that arise in the context of failures refinement (see Sect. 9.3.3). In this chapter we consider failures refinement in more depth, and in particular start to discuss the role that inputs and outputs have in a relational framework and how they correspond to aspects of divergence and refusals.

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

References

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

    Article  Google Scholar 

  2. He Jifeng (1989) Process refinement. In: McDermid J (ed) The theory and practice of refinement. Butterworths, Boston

    Google Scholar 

  3. Woodcock JCP, Morgan CC (1990) Refinement of state-based concurrent systems. In: Bjorner D, Hoare CAR, Langmaack H (eds) VDM’90: VDM and Z!- formal methods in software development. Lecture notes in computer science, vol 428. Springer, Berlin, pp 340–351

    Google Scholar 

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

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

    Article  Google Scholar 

  6. Smith G (1997) A semantic integration of Object-Z and CSP for the specification of concurrent systems. In: Fitzgerald J, Jones CB, Lucas P (eds) FME’97: industrial application and strengthened foundations of formal methods. Lecture notes in computer science, vol 1313. Springer, Berlin, pp 62–81

    Google Scholar 

  7. Smith G, Derrick J (2001) Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Formal Methods Syst Design 18:249–284

    Article  Google Scholar 

  8. Derrick J, Smith G (2000) Structural refinement in Object-Z/CSP. In: Grieskamp W, Santen T, Stoddart B (eds) International conference on integrated formal methods 2000 (IFM’00). Lecture notes in computer science, vol 1945. Springer, Berlin, pp 194–213

    Google Scholar 

  9. Fischer C (1997) CSP-OZ - A combination of CSP and Object-Z. In: Bowman H, Derrick J (eds) Second IFIP international conference on formal methods for open object-based distributed systems. Chapman & Hall, New York, pp 423–438

    Chapter  Google Scholar 

  10. Mahony BP, Dong JS (1998) Blending Object-Z and timed CSP: an introduction to TCOZ. In: Futatsugi K, Kemmerer R, Torii K (eds) 20th international conference on software engineering (ICSE’98). IEEE Press, New Jercy

    Google Scholar 

  11. Galloway A, Stoddart W, An operational semantics for ZCCS. In: Hinchey and Liu [23], pp 272–282

    Google Scholar 

  12. Treharne H, Schneider S, Using a process algebra to control B operations. In: Araki et al [21], pp 437–456

    Google Scholar 

  13. Fischer C, How to combine Z with a process algebra. In: Bowen et al [22], pp 5–23

    Google Scholar 

  14. Fischer C, Wehrheim H (2000) Behavioural subtyping relations for object-oriented formalisms. In: Rus T (ed) Algebraic methodology and software technology. Lecture notes in computer science, vol 1816. Springer, Berlin, pp 469–483

    Google Scholar 

  15. Wehrheim H (2000) Behavioural subtyping and property preservation. In: Smith SF, Talcott CL (eds) Formal methods for open object-based distributed systems (FMOODS 2000). Kluwer, The Netherlands, pp 213–231

    Google Scholar 

  16. Liskov B, Wing JM (1994) A behavioural notion of subtyping. ACM Trans Program Lang Syst 16(6):1811–1841

    Article  Google Scholar 

  17. Smith G, Derrick J, Refinement and verification of concurrent systems specified in Object-Z and CSP. In: Hinchey and Liu [101], pp 293–302

    Google Scholar 

  18. Bolton C, Davies J, Woodcock JCP, On the refinement and simulation of data types and processes. In: Araki et al [21], pp 273–292

    Google Scholar 

  19. Fischer C (2000) Combination and implementation of processes and data: from CSP-OZ to Java. PhD thesis, University of Oldenburg

    Google Scholar 

  20. Smith G, Derrick J (2002) Abstract specification in Object-Z and CSP. In: George C, Miao H (eds) Formal methods and software engineering. Lecture notes in computer science, vol 2495. Springer, Berlin, pp 108–119

    Google Scholar 

  21. Araki K, Galloway A, Taguchi K (eds) (1999) International conference on integrated formal methods 1999 (IFM’99). Springer, New York

    Google Scholar 

  22. Bowen JP, Fett A, Hinchey MG (eds) (1998) ZUM’98: The Z formal specification notation. Lecture notes in computer science, vol 1493. Springer, Berlin

    Google Scholar 

  23. Hinchey MG, Liu S (eds) (1997) First international conference on formal engineering methods (ICFEM’97). IEEE Computer Society Press, Hiroshima, Japan

    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). Relating Data Refinement and Failures-Divergences Refinement. In: Refinement. Springer, Cham. https://doi.org/10.1007/978-3-319-92711-4_10

Download citation

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

  • 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