{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:50:36Z","timestamp":1725558636968},"publisher-location":"Berlin, Heidelberg","reference-count":52,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203032"},{"type":"electronic","value":"9783540396567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39656-7_15","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T18:35:52Z","timestamp":1277836552000},"page":"361-379","source":"Crossref","is-referenced-by-count":2,"title":["Specification and Inheritance in CSP-OZ"],"prefix":"10.1007","author":[{"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Foundations of Object-Oriented Languages","author":"P. America","year":"1991","unstructured":"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.\u00a0489. Springer, Heidelberg (1991)"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T. Bolognesi","year":"1987","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems\u00a014, 25\u201359 (1987)","journal-title":"Computer Networks and ISDN Systems"},{"issue":"11","key":"15_CR3","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1109\/MCOM.2002.1047001","volume":"40","author":"J. Bredereke","year":"2002","unstructured":"Bredereke, J.: Maintaining telephone switching software requirements. IEEE Communications Magazine\u00a040(11), 104\u2013109 (2002)","journal-title":"IEEE Communications Magazine"},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"S.D. Brookes","year":"1984","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the ACM\u00a031, 560\u2013599 (1984)","journal-title":"Journal of the ACM"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-45685-6_8","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Brucker","year":"2002","unstructured":"Brucker, A., Wolff, B.: A proposal for a formal OCL semantics in Isabelle\/HOL. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, p. 99. Springer, Heidelberg (2002)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1007\/3-540-48119-2_28","volume-title":"FM\u201999 - Formal Methods","author":"M. Butler","year":"1999","unstructured":"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.\u00a01708, pp. 490\u2013508. Springer, Heidelberg (1999)"},{"key":"15_CR7","volume-title":"Parallel Program Design \u2013 A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design \u2013 A Foundation. Addison-Wesley, Reading (1988)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-540-39656-7_3","volume-title":"Formal Methods for Components and Objects","author":"W. Damm","year":"2003","unstructured":"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.\u00a02852, pp. 71\u201398. Springer, Heidelberg (2003)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-540-39656-7_4","volume-title":"Formal Methods for Components and Objects","author":"W. Damm","year":"2003","unstructured":"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.\u00a02852, pp. 99\u2013135. Springer, Heidelberg (2003)"},{"issue":"4","key":"15_CR10","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/s001650070012","volume":"12","author":"B.T. Denvir","year":"2000","unstructured":"Denvir, B.T., Oliveira, J., Plat, N.: The Cash-Point (ATM) Problem. Formal Aspects of Computing\u00a012(4), 211\u2013215 (2000)","journal-title":"Formal Aspects of Computing"},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1016\/0920-5489(95)00024-O","volume":"17","author":"R. Duke","year":"1995","unstructured":"Duke, R., Rose, G., Smith, G.: Object-Z: A specification language advocated for the description of standards. Computer Standards and Interfaces\u00a017, 511\u2013533 (1995)","journal-title":"Computer Standards and Interfaces"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/3-540-45314-8_8","volume-title":"Fundamental Approaches to Software Engineering","author":"C. Fischer","year":"2001","unstructured":"Fischer, C., Olderog, E.-R., Wehrheim, H.: A CSP view on UML-RT structure diagrams. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, pp. 91\u2013108. Springer, Heidelberg (2001)"},{"key":"15_CR13","first-page":"503","volume-title":"Proceedings of FORTE\/PSTV 1997","author":"C. Fischer","year":"1997","unstructured":"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\u2013518. Chapmann & Hall, Boca Raton (1997)"},{"key":"15_CR14","first-page":"315","volume-title":"Integrated Formal Methods","author":"C. Fischer","year":"1999","unstructured":"Fischer, C., Wehrheim, H.: Model-checking CSP-OZ specifications with FDR. In: Araki, K., Galloway, A., Taguchi, K. (eds.) Integrated Formal Methods, pp. 315\u2013334. Springer, Heidelberg (1999)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/3-540-45499-3_33","volume-title":"Algebraic Methodology and Software Technology","author":"C. Fischer","year":"2000","unstructured":"Fischer, C., Wehrheim, H.: Behavioural subtyping relations for object-oriented formalisms. In: Rus, T. (ed.) AMAST 2000. LNCS, vol.\u00a01816, pp. 469\u2013483. Springer, Heidelberg (2000)"},{"key":"15_CR16","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-0-387-35261-9_29","volume-title":"Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997)","author":"C. Fischer","year":"1997","unstructured":"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.\u00a02, pp. 423\u2013438. Chapman & Hall, Boca Raton (1997)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-49676-2_2","volume-title":"ZUM \u201998: The Z Formal Specification Notation","author":"C. Fischer","year":"1998","unstructured":"Fischer, C.: How to combine Z with a process algebra. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol.\u00a01493, pp. 5\u201323. Springer, Heidelberg (1998)"},{"unstructured":"Fischer, C.: Combination and Implementation of Processes and Data: From CSPOZ to Java. PhD thesis, Bericht Nr. 2\/2000, University of Oldenburg (April 2000)","key":"15_CR18"},{"key":"15_CR19","volume-title":"Int. Conf. of Formal Engineering Methods (ICFEM)","author":"A.J. Galloway","year":"1997","unstructured":"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)"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44685-0_5","volume-title":"CONCUR 2001 - Concurrency Theory","author":"J. Hatcliff","year":"2001","unstructured":"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.\u00a02154, p. 39. Springer, Heidelberg (2001)"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/3-540-45251-6_3","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"S. Helke","year":"2001","unstructured":"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.\u00a02021, p. 20. Springer, Heidelberg (2001)"},{"key":"15_CR22","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. CACM\u00a021, 666\u2013677 (1978)","journal-title":"CACM"},{"key":"15_CR23","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/3-540-47884-1_14","volume-title":"Integrated Formal Methods","author":"J. Hoenicke","year":"2002","unstructured":"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.\u00a02335, pp. 245\u2013266. Springer, Heidelberg (2002)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java Program Verification via a Hoare Logic with Abrupt Termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, pp. 284\u2013303. Springer, Heidelberg (2000)"},{"unstructured":"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\/","key":"15_CR26"},{"unstructured":"Kolyang. HOL-Z \u2013 An Integrated Formal Support Environment for Z in Isabelle\/ HOL. PhD thesis, Univ. Bremen, 1997. Shaker Verlag, Aachen (1999)","key":"15_CR27"},{"key":"15_CR28","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/s001659970003","volume":"11","author":"D. Latella","year":"1999","unstructured":"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\u00a011, 430\u2013445 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"15_CR29","doi-asserted-by":"crossref","first-page":"705","DOI":"10.1007\/BF01178658","volume":"32","author":"G.T. Leavens","year":"1995","unstructured":"Leavens, G.T., Weihl, W.E.: Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica\u00a032, 705\u2013778 (1995)","journal-title":"Acta Informatica"},{"key":"15_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/3-540-44577-3_11","volume-title":"Informatics","author":"K.R.M. Leino","year":"2001","unstructured":"Leino, K.R.M.: Extended static checking: A ten-year perspective. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol.\u00a02000, pp. 157\u2013175. Springer, Heidelberg (2001)"},{"issue":"6","key":"15_CR31","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B. Liskov","year":"1994","unstructured":"Liskov, B., Wing, J.: A behavioural notion of subtyping. ACM Transactions on Programming Languages and Systems\u00a016(6), 1811\u20131841 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR32","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1109\/ICSE.1998.671106","volume-title":"The 20th International Conference on Software Engineering (ICSE 1998)","author":"B.P. Mahony","year":"1998","unstructured":"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\u2013104. IEEE Computer Society Press, Los Alamitos (1998)"},{"doi-asserted-by":"crossref","unstructured":"Mota, A., Sampaio, A.: Model-checking CSP-Z: strategy, tool support and industrial application. Science of Computer Programming\u00a040(1) (2001)","key":"15_CR33","DOI":"10.1016\/S0167-6423(00)00023-X"},{"key":"15_CR34","first-page":"99","volume-title":"Object-oriented software composition","author":"O. Nierstrasz","year":"1995","unstructured":"Nierstrasz, O.: Regular types for active objects. In: Nierstrasz, O., Tsichritzis, D. (eds.) Object-oriented software composition, pp. 99\u2013121. Prentice Hall, Englewood Cliffs (1995)"},{"key":"15_CR35","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/BF00268075","volume":"23","author":"E.-R. Olderog","year":"1986","unstructured":"Olderog, E.-R., Hoare, C.A.R.: Specification-oriented semantics for communicating processes. Acta Inform.\u00a023, 9\u201366 (1986)","journal-title":"Acta Inform."},{"issue":"3","key":"15_CR36","first-page":"208","volume":"5","author":"A. Poetzsch-Heffter","year":"1999","unstructured":"Poetzsch-Heffter, A., Meyer, J.: Interactive verification environments for objectoriented languages. Journal of Universal Computer Science\u00a05(3), 208\u2013225 (1999)","journal-title":"Journal of Universal Computer Science"},{"key":"15_CR37","first-page":"353","volume-title":"A Classical Mind \u2014 Essays in Honour of C.A.R.Hoare","author":"A.W. Roscoe","year":"1994","unstructured":"Roscoe, A.W.: Model-checking CSP. In: Roscoe, A.W. (ed.) A Classical Mind \u2014 Essays in Honour of C.A.R.Hoare, pp. 353\u2013378. Prentice-Hall, Englewood Cliffs (1994)"},{"key":"15_CR38","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)"},{"key":"15_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/BFb0027284","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"M. Saaltink","year":"1997","unstructured":"Saaltink, M.: The Z\/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol.\u00a01212, pp. 72\u201388. Springer, Heidelberg (1997)"},{"doi-asserted-by":"crossref","unstructured":"Sch\u00e4fer, T., Knapp, A., Merz, S.: Model Checking UML State Machines and Collaborations. In: Workshop on Software Model Checking. ENTCS, vol.\u00a055 (2001)","key":"15_CR40","DOI":"10.1016\/S1571-0661(04)00262-2"},{"key":"15_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45648-1_5","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"G. Smith","year":"2002","unstructured":"Smith, G., Kamm\u00fcller, 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.\u00a02272, pp. 82\u201399. Springer, Heidelberg (2002)"},{"key":"15_CR42","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BF01211075","volume":"7","author":"G. Smith","year":"1995","unstructured":"Smith, G.: A fully abstract semantics of classes for Object-Z. Formal Aspects of Computing\u00a07, 289\u2013313 (1995)","journal-title":"Formal Aspects of Computing"},{"key":"15_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-63533-5_4","volume-title":"FME \u201997 Industrial Applications and Strengthened Foundations of Formal Methods","author":"G. Smith","year":"1997","unstructured":"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.\u00a01313, pp. 62\u201381. Springer, Heidelberg (1997)"},{"key":"15_CR44","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-5265-9","volume-title":"The Object-Z Specification Language","author":"G. Smith","year":"2000","unstructured":"Smith, G.: The Object-Z Specification Language. Kluwer Academic Publisher, Dordrecht (2000)"},{"key":"15_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/3-540-47884-1_15","volume-title":"Integrated Formal Methods","author":"G. Smith","year":"2002","unstructured":"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.\u00a02335, pp. 267\u2013285. Springer, Heidelberg (2002)"},{"unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall International Series in Computer Science (1992)","key":"15_CR46"},{"unstructured":"Taguchi, K., Araki, K.: Specifying concurrent systems by Z + CCS. In: International Symposium on Future Software Technology (ISFST), pp. 101\u2013108 (1997)","key":"15_CR47"},{"issue":"1-2","key":"15_CR48","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/S0304-3975(00)00321-2","volume":"270","author":"W.M.P. Aalst van der","year":"2002","unstructured":"van der Aalst, W.M.P., Basten, T.: Inheritance of Workflows \u2013 An approach to tackling problems related to change. Theoretical Computer Science\u00a0270(1-2), 125\u2013203 (2002)","journal-title":"Theoretical Computer Science"},{"key":"15_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-46428-X_23","volume-title":"Fundamental Approaches to Software Engineering","author":"H. Wehrheim","year":"2000","unstructured":"Wehrheim, H.: Specification of an automatic manufacturing system \u2013 a case study in using integrated formal methods. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, pp. 334\u2013348. Springer, Heidelberg (2000)"},{"unstructured":"Wehrheim, H.: Behavioural subtyping in object-oriented specification formalisms. University of Oldenburg, Habilitation Thesis (2002)","key":"15_CR50"},{"key":"15_CR51","first-page":"79","volume-title":"FMOODS 2002: Formal Methods for Open Object-Based Distributed Systems","author":"H. Wehrheim","year":"2002","unstructured":"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\u201393. Kluwer, Dordrecht (2002)"},{"key":"15_CR52","volume-title":"Using Z \u2014 Specification, Refinement, and Proof","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z \u2014 Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39656-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T14:57:09Z","timestamp":1559228229000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39656-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203032","9783540396567"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39656-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}