Advertisement

Process Refinement in B

  • Steve Dunne
  • Stacey Conroy
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)

Abstract

We describe various necessary and sufficient conditions with which to augment B’s existing refinement proof obligations for forward and backward refinement in order to capture within the B Method a variety of CSP process refinement relations, including most significantly that of failures-divergences which provides the standard denotational semantics of CSP processes.

Keywords

Label Transition System Proof Obligation Abstract Machine Abstract System Concrete State 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  2. 2.
    Abrial, J.-R.: Extending B without changing it (for developing distributed systems). In: Habrias, H. (ed.) Proceedings of the First B Conference, IRIN, Nantes, pp. 169–190 (1996)Google Scholar
  3. 3.
    Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  4. 4.
    Back, R.J.R., Kurki-Suonio, R.: Decentralisation of process nets with centralised control. In: 2nd ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pp. 131–142 (1983)Google Scholar
  5. 5.
    Bolton, C., Davies, J.: A comparison of refinement orderings and their associated simulation rules. In: Derrick, J., Boiten, E., Woodcock, J., Wright, J.v. (eds.) REFINE 2002 Proceedings. Electronic Notes in Theoretical Computer Science, vol. 70. Elsevier, Amsterdam (2002), http://www.elsevier.nl/locate/entcs Google Scholar
  6. 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)CrossRefGoogle Scholar
  7. 7.
    Bolton, C., Davies, J., Woodcock, J.C.P.: On the refinement and simulation of data types and processes. In: Araki, K., Galloway, A., Tagushi, K. (eds.) IFM 1999, 1st International Conference on Integrated Formal Methods, pp. 273–292. Springer, Heidelberg (1999)Google Scholar
  8. 8.
    Butler, M.: An approach to the design of distributed systems with B AMN. In: Till, D., P. Bowen, J., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 223–241. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  9. 9.
    Butler, M.: csp2B: a practial approach to combining CSP and B. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 490–508. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  10. 10.
    Butler, M., Waldén, M.: Distributed system development in B. In: Habrias, H. (ed.) Proceedings of the First B Conference, IRIN, Nantes, pp. 155–168 (1996)Google Scholar
  11. 11.
    Derrick, J., Boiten, E.: Refinement in Z and Object-Z. Springer, Heidelberg (2001)zbMATHGoogle Scholar
  12. 12.
    Derrick, J., Boiten, E.: Unifying concurrent and relational refinement. In: Derrick, J., Boiten, E., Woodcock, J., von Wright, J. (eds.) REFINE 2002 Proceedings. Electronic Notes in Theoretical Computer Science, vol.  70, Elsevier, Amsterdam (2002), http://www.elsevier.nl/locate/entcs Google Scholar
  13. 13.
    Derrick, J., Boiten, E.: Relational concurrent refinement. Formal Aspects of Computing 15, 182–214 (2003)zbMATHCrossRefGoogle Scholar
  14. 14.
    Derrick, J., Smith, G.: Structural refinement of systems specified in Object-Z and CSP. Formal Aspects of Computing 15, 1–27 (2003)zbMATHCrossRefGoogle Scholar
  15. 15.
    Dunne, S.E.: A theory of generalised substitutions. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 270–290. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  16. 16.
    Dunne, S.E.: Introducing backward refinement into B. In: Bert, D., Bowen, J. P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 178–196. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  17. 17.
    Fischer, C.: Combination and Implementation of Processes and Data: from CSP-OZ to Java. PhD thesis, University of Oldenburg (2000)Google Scholar
  18. 18.
    Jifeng, H.: Process refinement. In: Refinement Workshop, University of York (1988)Google Scholar
  19. 19.
    Jifeng, H.: Process refinement. In: McDermid, J. (ed.) The Theory and Practice of Refinement, Butterworths (1989)Google Scholar
  20. 20.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  21. 21.
    Jifengand, H., Hoare, C.A.R.: Prespecification and data refinement. In: Data Refinement in a Categorical Setting, Technical Monograph PRG-90. Oxford University Computing Laboratory (1990)Google Scholar
  22. 22.
    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)Google Scholar
  23. 23.
    Josephs, M.B.: A state-based approach to communicating processes. Distributed Computing 3, 9–18 (1988)zbMATHCrossRefGoogle Scholar
  24. 24.
    Milner, A.J.R.G.: Foreword. In: Roscoe, A.W. (ed.) A Classical Mind: essays in honour of C.A.R. Hoare. Prentice-Hall, Englewood Cliffs (1994)Google Scholar
  25. 25.
    Morgan, C.C.: Of wp and CSP. In: Feijen, W.H.J., van Gasteren, A.J.M., Gries, D., Misra, J. (eds.) Beauty is our business: a birthday salute to Edsger W. Dijkstra, pp. 319–326. Springer, Heidelberg (1990)Google Scholar
  26. 26.
    Phillips, I.C.C.: Refusals testing. Theoretical Computer Science 50, 241–284 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  28. 28.
    Rouzaud, Y.: Interpreting the B-Method in the Refinement Calculus. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 411–430. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  29. 29.
    Schneider, S.: Concurrent and Real-time Systems: the CSP approach. Wiley, Chichester (1999)Google Scholar
  30. 30.
    Schneider, S.: Non-blocking data refinement and traces-divergences semantics. Technical report CS-04-09, Department of Computing. University of Surrey (2004)Google Scholar
  31. 31.
    Schneider, S., Treharne, H.: Communicating B machines. In: Bert, D., Bowen, J. P., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 416–435. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  32. 32.
    Schneider, S., Treharne, H.: Verifying controlled components. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 87–107. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  33. 33.
    Smith, G.: The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, Dordrecht (2000)zbMATHGoogle Scholar
  34. 34.
    Smith, G., Derrick, J.: Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Formal Methods in System Design 18, 249–284 (2001)zbMATHCrossRefGoogle Scholar
  35. 35.
    Spivey, J.M.: The Z Notation: a Reference Manual, 2nd edn. Prentice-Hall, Englewood Cliffs (1992)Google Scholar
  36. 36.
    Treharne, H., Schneider, S.: How to drive a B machine. In: Bowen, J. P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, pp. 188–208. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  37. 37.
    Treharne, H., Schneider, S., Bramble, M.: Composing specifications using communication. In: Bert, D., Bowen, J. P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 58–78. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  38. 38.
    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, Elsevier, Amsterdam (2001)Google Scholar
  39. 39.
    Waldén, M.: Layering distributed algorithms within the B method. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 243–260. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  40. 40.
    Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice-Hall, Englewood Cliffs (1996)zbMATHGoogle Scholar
  41. 41.
    Woodcock, J.C.P., Morgan, C.C.: Refinement of state-based concurrent systems. In: Langmaack, H., Hoare, C.A.R., Bjorner, D. (eds.) VDM 1990. LNCS, vol. 428, pp. 340–351. Springer, Heidelberg (1990)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Steve Dunne
    • 1
  • Stacey Conroy
    • 1
  1. 1.School of ComputingUniversity of TeessideMiddlesbroughUK

Personalised recommendations