Modelling Divergence in Relational Concurrent Refinement | SpringerLink
Skip to main content
Springer Nature Link
Log in

Modelling Divergence in Relational Concurrent Refinement

  • Conference paper
Integrated Formal Methods (IFM 2009)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5423))

Included in the following conference series:

Abstract

An integration of state-based and behavioural formalisms can be obtained by imposing a concurrency semantics on a relational formalism. The data refinement theory for relational languages then provides a method for verifying the concurrent refinement relation. In this paper we investigate how divergence can be modelled relationally, and in particular show how differing process algebraic interpretations of divergence can be embedded in a relational framework. In doing so we derive relational simulation conditions for process algebraic refinement incorporating divergence.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abramsky, S.: Observation equivalence as a testing equivalence. Theor. Comput. Sci. 53(2-3), 225–241 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier Science Inc., New York (2001)

    MATH  Google Scholar 

  3. Boiten, E.A., Derrick, J.: Incompleteness of relational simulations in the blocking paradigm (submitted for publication, 2008)

    Google Scholar 

  4. Boiten, E.A., Derrick, J., Schellhorn, G.: Relational concurrent refinement II: Internal operations and outputs. Formal Aspects of Computing (accepted for publication)

    Google Scholar 

  5. Bolognesi, T., Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems 14(1), 25–59 (1988)

    Article  Google Scholar 

  6. Bolton, C., Davies, J.: Refinement in Object-Z and CSP. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 225–244. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  7. Brinksma, E., Scollo, G.: Formal notions of implementation and conformance in LOTOS. Technical Report INF-86-13, Dept of Informatics, Twente University of Technology (1986)

    Google Scholar 

  8. Brinksma, E., Scollo, G., Steenbergen, C.: Process specification, their implementation and their tests. In: Sarikaya, B., Bochmann, G.v. (eds.) Protocol Specification, Testing and Verification, VI, Montreal, Canada, jun 1986, pp. 349–360. North-Holland, Amsterdam (1986)

    Google Scholar 

  9. Butler, M.: An approach to the design of distributed systems with B AMN. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 223–241. Springer, Heidelberg (1997)

    Google Scholar 

  10. Cleaveland, R., Hennessy, M.: Testing equivalence as a bisimulation equivalence. In: Proceedings of the international workshop on Automatic verification methods for finite state systems, pp. 11–23. Springer, New York (1990)

    Chapter  Google Scholar 

  11. de Nicola, R.: Extensional equivalences for transition systems. Acta Informatica 24(2), 211–237 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  12. de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)

    Book  MATH  Google Scholar 

  13. Derrick, J., Boiten, E.A.: Refinement in Z and Object-Z. Springer, Heidelberg (2001)

    Book  MATH  Google Scholar 

  14. Derrick, J., Boiten, E.A.: Relational concurrent refinement. Formal Aspects of Computing 15(1), 182–214 (2003)

    Article  MATH  Google Scholar 

  15. Derrick, J., Boiten, E.A.: Relational concurrent refinement with internal operations. In: Aichernig, B., Boiten, E.A., Derrick, J., Groves, L. (eds.) BCS-FACS Refinement Workshop. ENTCS, vol. 187, pp. 35–53 (2006)

    Google Scholar 

  16. Derrick, J., Boiten, E.A.: More relational concurrent refinement: traces and partial relations. In: Boiten, E.A., Derrick, J., Schellhorn, G. (eds.) Proceedings REFINE. ENTCS (to appear, 2008)

    Google Scholar 

  17. Derrick, J., Boiten, E.A., Bowman, H., Steen, M.: Specifying and Refining Internal Operations in Z. Formal Aspects of Computing 10, 125–159 (1998)

    Article  MATH  Google Scholar 

  18. van Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990)

    Google Scholar 

  19. van Glabbeek, R.J.: The linear time – branching time spectrum II; the semantics of sequential systems with silent moves (extended abstract). In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)

    Google Scholar 

  20. van Glabbeek, R.J.: The linear time - branching time spectrum I. The semantics of concrete sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 3–99. North-Holland, Amsterdam (2001)

    Chapter  Google Scholar 

  21. Jifeng, H., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)

    Chapter  Google Scholar 

  22. Hennessy, M.: Algebraic theory of processes. MIT Press, Cambridge (1988)

    MATH  Google Scholar 

  23. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  24. Josephs, M.B.: A state-based approach to communicating processes. Distributed Computing 3, 9–18 (1988)

    Article  MATH  Google Scholar 

  25. Leduc, G.: On the Role of Implementation Relations in the Design of Distributed Systems using LOTOS. PhD thesis, University of Liège, Liège, Belgium (June 1991)

    Google Scholar 

  26. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  27. De Nicola, R., Hennessy, M.: Testing equivalence for processes. In: Díaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 548–560. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  28. Puhakka, A., Valmari, A.: Weakest-congruence results for livelock-preserving equivalences. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 510–524. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  29. Reeves, S., Streader, D.: Data refinement and singleton failures refinement are not equivalent. Formal Aspects of Computing 20(3), 295–301 (2008)

    Article  MATH  Google Scholar 

  30. Roscoe, A.W.: The Theory and Practice of Concurrency. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  31. Roscoe, A.W.: Seeing beyond divergence. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. LNCS, vol. 3525, pp. 15–35. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  32. Woodcock, J.C.P., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing Laboratory, University of Kent, Canterbury, Kent, UK

    Eerke Boiten

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

    John Derrick

Authors
  1. Eerke Boiten
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John Derrick
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, Universitätsstraße 1, 40225, Düsseldorf, Germany

    Michael Leuschel

  2. Fakultät für Elektrotechnik, Informatik und Mathematik, Universität Paderborn, Warburger Straße 100, 33098, Paderborn, Germany

    Heike Wehrheim

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Boiten, E., Derrick, J. (2009). Modelling Divergence in Relational Concurrent Refinement. In: Leuschel, M., Wehrheim, H. (eds) Integrated Formal Methods. IFM 2009. Lecture Notes in Computer Science, vol 5423. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00255-7_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-00255-7_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-00254-0

  • Online ISBN: 978-3-642-00255-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics