Advertisement

Specification and Inheritance in CSP-OZ

  • Ernst-Rüdiger Olderog
  • Heike Wehrheim
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2852)

Abstract

CSP-OZ [16,18] is a combination of Communicating Sequential Processes (CSP) and Object-Z (OZ). It enables the specification of systems having both a state-based and a behaviour-oriented view using the object-oriented concepts of classes, instantiation and inheritance. CSP-OZ has a process semantics in the failures divergence model of CSP. In this paper we explain CSP-OZ and investigate the notion of inheritance. Behavioural subtyping relations between classes introduced in [50] guarantee the inheritance of safety and ”liveness” properties.

Keywords

CSP Object-Z failure divergence semantics inheritance safety and ”liveness” properties model-checking FDR 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    America, P.: Designing an object-oriented programming language with behavioural subtyping. In: de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1990. LNCS, vol. 489. Springer, Heidelberg (1991)Google Scholar
  2. 2.
    Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems 14, 25–59 (1987)CrossRefGoogle Scholar
  3. 3.
    Bredereke, J.: Maintaining telephone switching software requirements. IEEE Communications Magazine 40(11), 104–109 (2002)CrossRefGoogle Scholar
  4. 4.
    Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the ACM 31, 560–599 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Brucker, A., Wolff, B.: A proposal for a formal OCL semantics in Isabelle/HOL. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, p. 99. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    Butler, M.: csp2B: A practical 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
  7. 7.
    Chandy, K.M., Misra, J.: Parallel Program Design – A Foundation. Addison-Wesley, Reading (1988)zbMATHGoogle Scholar
  8. 8.
    Damm, W., Josko, B., Pnueli, A., Votintseva, A.: Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 71–98. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Damm, W., Westphal, B.: Live and Let Die: LSC-based Verification of UMLModels. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 99–135. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    Denvir, B.T., Oliveira, J., Plat, N.: The Cash-Point (ATM) Problem. Formal Aspects of Computing 12(4), 211–215 (2000)CrossRefGoogle Scholar
  11. 11.
    Duke, R., Rose, G., Smith, G.: Object-Z: A specification language advocated for the description of standards. Computer Standards and Interfaces 17, 511–533 (1995)CrossRefGoogle Scholar
  12. 12.
    Fischer, C., Olderog, E.-R., Wehrheim, H.: A CSP view on UML-RT structure diagrams. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 91–108. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  13. 13.
    Fischer, C., Smith, G.: Combining CSP and Object-Z: Finite or infinite tracesemantics? In: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A. (eds.) Proceedings of FORTE/PSTV 1997, pp. 503–518. Chapmann & Hall, Boca Raton (1997)Google Scholar
  14. 14.
    Fischer, C., Wehrheim, H.: Model-checking CSP-OZ specifications with FDR. In: Araki, K., Galloway, A., Taguchi, K. (eds.) Integrated Formal Methods, pp. 315–334. Springer, Heidelberg (1999)Google Scholar
  15. 15.
    Fischer, C., Wehrheim, H.: Behavioural subtyping relations for object-oriented formalisms. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 469–483. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  16. 16.
    Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: Bowman, H., Derrick, J. (eds.) Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997), vol. 2, pp. 423–438. Chapman & Hall, Boca Raton (1997)Google Scholar
  17. 17.
    Fischer, C.: How to combine Z with a process algebra. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 5–23. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  18. 18.
    Fischer, C.: Combination and Implementation of Processes and Data: From CSPOZ to Java. PhD thesis, Bericht Nr. 2/2000, University of Oldenburg (April 2000)Google Scholar
  19. 19.
    Galloway, A.J., Stoddart, W.: An operational semantics for ZCCS. In: Hinchey, M., Liu, S. (eds.) Int. Conf. of Formal Engineering Methods (ICFEM), IEEE, Los Alamitos (1997)Google Scholar
  20. 20.
    Hatcliff, J., Dwyer, M.: Using the Bandera tool set to model-check properties of concurrent Java software. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, p. 39. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  21. 21.
    Helke, S., Santen, T.: Mechanized analysis of behavioral conformance in the Eiffel base libraries. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, p. 20. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  22. 22.
    Hoare, C.A.R.: Communicating sequential processes. CACM 21, 666–677 (1978)zbMATHGoogle Scholar
  23. 23.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  24. 24.
    Hoenicke, J., Olderog, E.-R.: Combining specification techniques for processes, data and time. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 245–266. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  25. 25.
    Huisman, M., Jacobs, B.: Java Program Verification via a Hoare Logic with Abrupt Termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  26. 26.
    ISO. Final comittee draft on enhancements to LOTOS. ISO/IEC JTC1/SC21, WG7 Enhancements to LOTOS (1998), ftp://ftp.dit.upm.es/pub/lotos/elotos/Working.Docs/
  27. 27.
    Kolyang. HOL-Z – An Integrated Formal Support Environment for Z in Isabelle/ HOL. PhD thesis, Univ. Bremen, 1997. Shaker Verlag, Aachen (1999)Google Scholar
  28. 28.
    Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects of Computing 11, 430–445 (1999)CrossRefGoogle Scholar
  29. 29.
    Leavens, G.T., Weihl, W.E.: Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica 32, 705–778 (1995)zbMATHMathSciNetGoogle Scholar
  30. 30.
    Leino, K.R.M.: Extended static checking: A ten-year perspective. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, pp. 157–175. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  31. 31.
    Liskov, B., Wing, J.: A behavioural notion of subtyping. ACM Transactions on Programming Languages and Systems 16(6), 1811–1841 (1994)CrossRefGoogle Scholar
  32. 32.
    Mahony, B.P., Dong, J.S.: Blending Object-Z and Timed CSP: An introduction to TCOZ. In: The 20th International Conference on Software Engineering (ICSE 1998), April 1998, pp. 95–104. IEEE Computer Society Press, Los Alamitos (1998)CrossRefGoogle Scholar
  33. 33.
    Mota, A., Sampaio, A.: Model-checking CSP-Z: strategy, tool support and industrial application. Science of Computer Programming 40(1) (2001)Google Scholar
  34. 34.
    Nierstrasz, O.: Regular types for active objects. In: Nierstrasz, O., Tsichritzis, D. (eds.) Object-oriented software composition, pp. 99–121. Prentice Hall, Englewood Cliffs (1995)Google Scholar
  35. 35.
    Olderog, E.-R., Hoare, C.A.R.: Specification-oriented semantics for communicating processes. Acta Inform. 23, 9–66 (1986)zbMATHCrossRefMathSciNetGoogle Scholar
  36. 36.
    Poetzsch-Heffter, A., Meyer, J.: Interactive verification environments for objectoriented languages. Journal of Universal Computer Science 5(3), 208–225 (1999)Google Scholar
  37. 37.
    Roscoe, A.W.: Model-checking CSP. In: Roscoe, A.W. (ed.) A Classical Mind — Essays in Honour of C.A.R.Hoare, pp. 353–378. Prentice-Hall, Englewood Cliffs (1994)Google Scholar
  38. 38.
    Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)Google Scholar
  39. 39.
    Saaltink, M.: The Z/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 72–88. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  40. 40.
    Schäfer, T., Knapp, A., Merz, S.: Model Checking UML State Machines and Collaborations. In: Workshop on Software Model Checking. ENTCS, vol. 55 (2001)Google Scholar
  41. 41.
    Smith, G., Kammüller, F., Santen, T.: Encoding Object-Z in Isabelle/HOL. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 82–99. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  42. 42.
    Smith, G.: A fully abstract semantics of classes for Object-Z. Formal Aspects of Computing 7, 289–313 (1995)CrossRefGoogle Scholar
  43. 43.
    Smith, G.: A semantic integration of Object-Z and CSP for the specification of cocurrent systems. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 62–81. Springer, Heidelberg (1997)Google Scholar
  44. 44.
    Smith, G.: The Object-Z Specification Language. Kluwer Academic Publisher, Dordrecht (2000)zbMATHGoogle Scholar
  45. 45.
    Smith, G.: An integration of real-time Object-Z and CSP for specifying concurrent real-time systems. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 267–285. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  46. 46.
    Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall International Series in Computer Science (1992)Google Scholar
  47. 47.
    Taguchi, K., Araki, K.: Specifying concurrent systems by Z + CCS. In: International Symposium on Future Software Technology (ISFST), pp. 101–108 (1997)Google Scholar
  48. 48.
    van der Aalst, W.M.P., Basten, T.: Inheritance of Workflows – An approach to tackling problems related to change. Theoretical Computer Science 270(1-2), 125–203 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  49. 49.
    Wehrheim, H.: Specification of an automatic manufacturing system – a case study in using integrated formal methods. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 334–348. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  50. 50.
    Wehrheim, H.: Behavioural subtyping in object-oriented specification formalisms. University of Oldenburg, Habilitation Thesis (2002)Google Scholar
  51. 51.
    Wehrheim, H.: Checking behavioural subtypes via refinement. In: Rensink, A., Jacobs, B. (eds.) FMOODS 2002: Formal Methods for Open Object-Based Distributed Systems, pp. 79–93. Kluwer, Dordrecht (2002)Google Scholar
  52. 52.
    Woodcock, J., Davies, J.: Using Z — Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Ernst-Rüdiger Olderog
    • 1
  • Heike Wehrheim
    • 1
  1. 1.Department of Computing ScienceUniversity of OldenburgOldenburgGermany

Personalised recommendations