{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:23:00Z","timestamp":1725560580171},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540213772"},{"type":"electronic","value":"9783540247562"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24756-2_15","type":"book-chapter","created":{"date-parts":[[2010,7,27]],"date-time":"2010-07-27T20:18:31Z","timestamp":1280261911000},"page":"267-286","source":"Crossref","is-referenced-by-count":14,"title":["Linking CSP-OZ with UML and Java: A Case Study"],"prefix":"10.1007","author":[{"given":"Michael","family":"M\u00f6ller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Rasch","sequence":"additional","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","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/3-540-45931-6_2","volume-title":"Foundations of Software Science and Computation Structures","author":"E. \u00c1brah\u00e1m-Mumm","year":"2002","unstructured":"\u00c1brah\u00e1m-Mumm, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: Verification for Java\u2019s reentrant multithreading concept. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 4\u201320. Springer, Heidelberg (2002)"},{"key":"15_CR2","volume-title":"ENTCS","author":"D. Bartetzko","year":"2001","unstructured":"Bartetzko, D., Fischer, C., M\u00f6ller, M., Wehrheim, H.: Jass \u2013 Java with Assertions. In: Havelund, K., Ro\u015fu, G. (eds.) ENTCS, vol.\u00a055, Elsevier, Amsterdam (2001), http:\/\/www.elsevier.nl\/locate\/entcs\/volume55.html"},{"key":"15_CR3","unstructured":"Breunesse, C.-B., Poll, E.: Verifying JML specifications with model fields. In: Workshop on Formal Techniques for Java-like Programs \u2013 FTfJP 2003. ETH Z\u00fcrich, Technical Report 108 (July 2003)"},{"key":"15_CR4","unstructured":"Br\u00f6rkens, M.: Trace- und Zeit-Zusicherungen beim Programmieren mit Vertrag. Master\u2019s thesis, Univ. of Oldenburg, Dept. of Computing Science (January 2002)"},{"key":"15_CR5","volume-title":"ENTCS","author":"M. Br\u00f6rkens","year":"2002","unstructured":"Br\u00f6rkens, M., M\u00f6ller, M.: Dynamic Event Generation for Runtime Checking using the JDI. In: Havelund, K., Rosu, G. (eds.) ENTCS, vol.\u00a070, Elsevier, Amsterdam (2002), http:\/\/www.elsevier.nl\/locate\/entcs\/volume70.html"},{"key":"15_CR6","volume-title":"Workshop on Formal Methods for Parallel Programming, held in conjunction with International Parallel and Distributed Processing Symposium","author":"A. Cavalcanti","year":"2002","unstructured":"Cavalcanti, A., Sampaio, A.: From CSP-OZ to Java with Processes. In: Workshop on Formal Methods for Parallel Programming, held in conjunction with International Parallel and Distributed Processing Symposium, IEEE CS Press, Los Alamitos (2002), Contained in IPDPS collects proceedings CD-ROM"},{"key":"15_CR7","volume-title":"ENTCS","author":"J. Davies","year":"2002","unstructured":"Davies, J., Crichton, C.: Concurrency and Refinement in the Unified Modeling Language. In: Derrick, J., Boiten, E., Woodcock, J., von Wright, J. (eds.) ENTCS, vol.\u00a070, Elsevier, Amsterdam (2002)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/10722468_19","volume-title":"SPIN Model Checking and Software Verification","author":"D. Drusinsky","year":"2000","unstructured":"Drusinsky, D.: The Temporal Rover and the ATG Rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 323\u2013330. Springer, Heidelberg (2000)"},{"key":"15_CR9","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_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/3-540-45140-4_28","volume-title":"Advanced Information Systems Engineering","author":"S. Dupuy","year":"2000","unstructured":"Dupuy, S., Ledru, Y., Chabre-Peccoud, M.: An overview of RoZ - a tool for integrating UML and Z specifications. In: Wangler, B., Bergman, L.D. (eds.) CAiSE 2000. LNCS, vol.\u00a01789, p. 417. Springer, Heidelberg (2000)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Engels, G., K\u00fcster, J., Heckel, R., Groenewegen, L.: A Methodology for Specifying and Analyzing Consistency of Object-Oriented Behavioral Models. In: 9th ACM SigSoft Symposium on Foundations of Software Engineering, ACM Software Engineering Notes, vol.\u00a026 (2001)","DOI":"10.1145\/503271.503235"},{"key":"15_CR12","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_CR13","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_CR14","first-page":"315","volume-title":"Proc. 1st International Conference on Integrated Formal Methods (IFM)","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.) Proc. 1st International Conference on Integrated Formal Methods (IFM), pp. 315\u2013334. Springer, Heidelberg (1999)"},{"key":"15_CR15","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn., June 2000. Addison-Wesley, Reading (2000)"},{"key":"15_CR16","unstructured":"Gullekson, G.: Designing for concurrency and distribution with Rational Rose RealTime. Technical report, Rational Software (2000)"},{"key":"15_CR17","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_CR18","series-title":"ENTCS","volume-title":"Monitoring Java Programs with Java Path Explorer","year":"2001","unstructured":"Havelund, K., Rosu, G. (eds.): Monitoring Java Programs with Java Path Explorer. ENTCS, vol.\u00a055. Elsevier, Amsterdam (2001)"},{"key":"15_CR19","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_CR20","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)"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Jacobs, B., van den Berg, J., van Berkum, M.H.M., Hensel, U., Tews, H.: Reasoning about Java classes (preliminary report). In: Proc. OOPSLA 1998, October 1998. ACM SIGPLAN Notices, vol.\u00a033, pp. 329\u2013340 (1998)","DOI":"10.1145\/286942.286973"},{"key":"15_CR22","unstructured":"Kramer, R.: iContract - the Java Design by Contract tool. Technical report, Reliable Systems (1998)"},{"key":"15_CR23","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_CR24","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for java. Technical Report 98-06v, Iowa State Univ., Dept. of Computer Science (May 2003), See, http:\/\/www.jmlspecs.org"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-39656-7_11","volume-title":"Formal Methods for Components and Objects","author":"G.T. Leavens","year":"2003","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accomodates both runtime assertion checking and formal verifikation. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 262\u2013284. Springer, Heidelberg (2003) (to appear)"},{"key":"15_CR26","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":"3","key":"15_CR27","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_CR28","unstructured":"M\u00f6ller, M.: Specifying and Checking Java using CSP. In: Workshop on Formal Techniques for Java-like Programs \u2013 FTfJP 2002. Computing Science Department, University of Nijmegen, Technical Report NIII-R0204 (June 2002)"},{"key":"15_CR29","unstructured":"Rasch, H.: Translating UML state machines into CSP. Technical report, Universit\u00e4t Oldenburg (2003)"},{"key":"15_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-39958-2_16","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"H. Rasch","year":"2003","unstructured":"Rasch, H., Wehrheim, H.: Checking Consistency in UML Diagrams: Classes and State Machines. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.\u00a02884, pp. 229\u2013243. Springer, Heidelberg (2003)"},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-46428-X_10","volume-title":"Fundamental Approaches to Software Engineering","author":"G. Reggio","year":"2000","unstructured":"Reggio, G., Astesiano, E., Choppy, C., Hussmann, H.: Analysing UML active classes and associated state machines \u2013 A lightweight formal approach. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, p. 127. Springer, Heidelberg (2000)"},{"key":"15_CR32","volume-title":"The Theory and Practice of Concurrency","author":"W. Roscoe","year":"1997","unstructured":"Roscoe, W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)"},{"key":"15_CR33","series-title":"Object Technology Series","volume-title":"The Unified Modeling Language Reference Manual","author":"J. Rumbaugh","year":"1999","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Object Technology Series. Addison-Wesley, Reading (1999)"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Sch\u00e4fer, T., Knapp, A., Merz, S.: Model Checking UML State Machines and Collaborations. In: Stoller, S.D., Visser, W. (eds.). ENTCS, vol.\u00a055, Elsevier, Amsterdam (2001)","DOI":"10.1016\/S1571-0661(04)00262-2"},{"key":"15_CR35","volume-title":"Real-Time Object-Oriented Modeling","author":"B. Selic","year":"1994","unstructured":"Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object-Oriented Modeling. John Wiley & Sons, Chichester (1994)"},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Selic, B., Rumbaugh, J.: Using UML for modeling complex real-time systems. Technical report, ObjecTime (1998)","DOI":"10.1007\/BFb0057795"},{"key":"15_CR37","unstructured":"Snook, C., Butler, M.: Tool-Supported Use of UML for Constructing B Specifications. Technical report, http:\/\/www.ecs.soton.ac.uk\/~mjb\/U2Bpaper2.pdf"},{"key":"15_CR38","unstructured":"OMG Unified Modeling Language specification, version 1.5 (March 2003), http:\/\/www.omg.org"},{"key":"15_CR39","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)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24756-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T15:33:20Z","timestamp":1559316800000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24756-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213772","9783540247562"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24756-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}