{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214707},"reference-count":69,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2008,3,1]],"date-time":"2008-03-01T00:00:00Z","timestamp":1204329600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2008,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We describe how CSP-OZ, a formal method combining the process algebra CSP with the specification language Object-Z, can be integrated into an object-oriented software engineering process employing the UML as a modelling and Java as an implementation language. The benefit of this integration lies in the rigour of the formal method, which improves the precision of the constructed models and opens up the possibility of (1) verifying properties of models in the early design phases, and (2) checking adherence of implementations to models.<\/jats:p>\n          <jats:p>\n            The envisaged application area of our approach is the design of distributed\n            <jats:italic>reactive systems<\/jats:italic>\n            . To this end, we propose a specific UML\n            <jats:italic>profile<\/jats:italic>\n            for reactive systems. The profile contains facilities for modelling components, their interfaces and interconnections via synchronous\/broadcast communication, and the overall architecture of a system. The integration with the formal method proceeds by generating a significant part of the CSP-OZ specification from the initially developed UML model. The formal specification is on the one hand the starting point for\n            <jats:italic>verifying<\/jats:italic>\n            properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating\n            <jats:italic>contracts<\/jats:italic>\n            for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by CSP\n            <jats:sub>jassda<\/jats:sub>\n            , an assertion language for specifying orderings between method invocations. A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts.\n          <\/jats:p>","DOI":"10.1007\/s00165-007-0042-7","type":"journal-article","created":{"date-parts":[[2007,7,18]],"date-time":"2007-07-18T10:45:50Z","timestamp":1184755550000},"page":"161-204","source":"Crossref","is-referenced-by-count":21,"title":["Integrating a formal method into a software engineering process with UML and Java"],"prefix":"10.1145","volume":"20","author":[{"given":"Michael","family":"M\u00f6ller","sequence":"first","affiliation":[{"name":"Department of Computing Science, University of Oldenburg, 26111, Oldenburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"additional","affiliation":[{"name":"Department of Computing Science, University of Oldenburg, 26111, Oldenburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Rasch","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Paderborn, 33098, Paderborn, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Paderborn, 33098, Paderborn, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m-Mumm E de Boer FS de Roever W-P Steffen M (2002) Verification for Java\u2019s reentrant multithreading concept. In: FoSSACS 2002 Vol 2303 of LNCS Springer Heidelberg pp 4\u201320","DOI":"10.1007\/3-540-45931-6_2"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bolton Ch Davies J (2002) Refinement in Object-Z and CSP. In: Butler M Petre L Sere K (eds) IFM 2002: integrated formal methods number 2335 in LNCS pp 225\u2013244","DOI":"10.1007\/3-540-47884-1_13"},{"key":"e_1_2_1_2_3_2","unstructured":"Bartetzko D Fischer C M\u00f6ller M Wehrheim H (2001) Jass\u2014Java with Assertions. In: Havelund K Ro\u015fu G (eds) ENTCS Vol 55. Elsevier http:\/\/www.elsevier.nl\/locate\/entcs\/volume55.html"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Br\u00f6rkens M M\u00f6ller M (2002) Dynamic event generation for runtime checking using the JDI. In: Havelund K Rosu G (eds) ENTCS Vol 70. Elsevier http:\/\/www.elsevier.nl\/locate\/entcs\/volume70.html","DOI":"10.1016\/S1571-0661(04)80575-9"},{"key":"e_1_2_1_2_6_2","unstructured":"Br\u00f6rkens M (2002) Trace- und Zeit-Zusicherungen beim Programmieren mit Vertrag. Master\u2019s thesis University of Oldenburg Department of Computing Science January 2002"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Cavalcanti A Sampaio A (2002) 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 2002. Contained in IPDPS collected proceedings CD-ROM","DOI":"10.1109\/IPDPS.2002.1016617"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0006-5"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0007-4"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0008-3"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011227529550"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Damm W Josko B Pnueli A Votintseva A (2005) A discrete-time UML semantics for concurrency and communication in safety-critical applications. Sci Comput Program 55(1-3)","DOI":"10.1016\/j.scico.2004.05.012"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Dupuy S Ledru Y Chabre-Peccoud M (2000) An overview of RoZ - a tool for integrating UML and Z specifications. In: 12th conference on advanced information systems engineering (CAiSE\u20192000)","DOI":"10.1007\/3-540-45140-4_28"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/0920-5489(95)00024-O"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Drusinsky D (2000) The Temporal Rover and the ATG Rover. In: SPIN Modelchecking and Software Verification volume 1885 of LNCS Springer Heidelberg pp 323\u2013330","DOI":"10.1007\/10722468_19"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Engels G K\u00fcster J Heckel R Groenewegen L (2001) A methodology for specifying and analyzing consistency of object-oriented behavioral models. In: 9th ACM SigSoft symposium on foundations of software engineering Vol 26 of ACM Software Engineering Notes","DOI":"10.1145\/503209.503235"},{"key":"e_1_2_1_2_17_2","unstructured":"Formal Systems (Europe) Ltd. (2003) Failures-divergence refinement: FDR2 user manual May 2003"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Fischer C (1997) CSP-OZ: a combination of Object-Z and CSP. In: Bowman H Derrick J (eds) Formal methods for open object-based distributed systems (FMOODS \u201997) Vol 2. Chapman & Hall London pp 423\u2013438","DOI":"10.1007\/978-0-387-35261-9_29"},{"key":"e_1_2_1_2_19_2","unstructured":"Fischer C (2000) Combination and implementation of processes and data: from CSP-OZ to Java. PhD thesis Bericht Nr. 2\/2000 University of Oldenburg April 2000"},{"key":"#cr-split#-e_1_2_1_2_20_2.1","doi-asserted-by":"crossref","unstructured":"Fischer C Olderog E-R Wehrheim H (2001) A CSP view on UML-RT structure diagrams. In: Hussmann H","DOI":"10.1007\/3-540-45314-8_8"},{"key":"#cr-split#-e_1_2_1_2_20_2.2","unstructured":"(ed) Fundamental approaches to software engineering (FASE'01) Vol 2029 of LNCS. Springer Heidelberg 2001 pp 91-108"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Fecher H Sch\u00f6nborn J Kyas M de Roever WP (2005) 29 new unclarities in the semantics of UML 2.0 state machines. In: ICFEM Vol 3785 of LNCS. Springer Heidelberg 2005 pp 52\u201365","DOI":"10.1007\/11576280_5"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Fischer C Wehrheim H (1999) Model-checking CSP-OZ specifications with FDR. In: Araki K Galloway A Taguchi K (eds) Proceedings of the first international conference on integrated formal methods (IFM). Springer pp 315\u2013334","DOI":"10.1007\/978-1-4471-0851-1_17"},{"key":"e_1_2_1_2_23_2","unstructured":"Gosling J Joy B Steele G Bracha G (2000) The Java language specification second edition. Addison-Wesley Reading"},{"key":"e_1_2_1_2_24_2","unstructured":"Gullekson G (2000) Designing for concurrency and distribution with Rational Rose RealTime. Technical report Rational Software"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Hatcliff J Dwyer M (2001) Using the Bandera tool set to model-check properties of concurrent Java software. In: Larsen KG (ed) CONCUR 2001 LNCS. Springer Heidelberg","DOI":"10.1007\/3-540-44685-0_5"},{"key":"#cr-split#-e_1_2_1_2_26_2.1","doi-asserted-by":"crossref","unstructured":"Huisman M Jacobs B (2000) Java program verification via a Hoare Logic with abrupt termination. In: Maibaum T","DOI":"10.1007\/3-540-46428-X_20"},{"key":"#cr-split#-e_1_2_1_2_26_2.2","unstructured":"(ed) Fundamental approaches to software engineering (FASE 2000) Vol 1783 of LNCS. Springer Heidelberg pp 284-303"},{"key":"e_1_2_1_2_27_2","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0117-6"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000017721.39909.4b"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Jacobs B van den Berg J Huisman M van Berkum M Hensel U Tews H (1998) Reasoning about Java classes (preliminary report). In: Proceedings OOPSLA 98 Vol 33 of ACM SIGPLAN notices pp 329\u2013340 Oct. 1998","DOI":"10.1145\/286942.286973"},{"key":"e_1_2_1_2_31_2","unstructured":"The Java Modeling Language (JML) home page. http:\/\/www.jmlspecs.org\/"},{"key":"e_1_2_1_2_32_2","unstructured":"Kramer R (1998) iContract\u2014the Java Design by Contract tool. Technical report Reliable Systems"},{"key":"e_1_2_1_2_33_2","unstructured":"Leavens GT Baker AL Ruby C (2003) 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":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Leavens GT Cheon Y Clifton C Ruby C Cok DR (2003) How the design of JML accomodates both runtime assertion checking and formal verification. In: FMCO\u201902 Vol 2852 of LNCS. Springer Heidelberg","DOI":"10.1007\/978-3-540-39656-7_11"},{"key":"e_1_2_1_2_35_2","first-page":"157","volume-title":"Informatics\u201410\u00a0years back, 10\u00a0years ahead, Vol 2000 of LNCS.","author":"Leino KRM","year":"2001"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Leuschel M Massart T Currie A (2001) How to make FDR spin: LTL model checking of CSP by refinement. In: FME 2001: international symposium of formal methods Europe Vol 2021 of LNCS. Springer Heidelberg","DOI":"10.1007\/3-540-45251-6_6"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001659970003"},{"key":"e_1_2_1_2_38_2","unstructured":"OMG model driven architecture. Object Management Group. http:\/\/www.omg.org\/mda"},{"key":"e_1_2_1_2_39_2","unstructured":"Meyer B (1997) Object-oriented software construction 2nd edn. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_40_2","unstructured":"M\u00f6ller M (2002) Specifying and checking Java using CSP. In: Workshop on formal techniques for java-like programs\u2014FTfJP\u20192002. Computing Science Department University of Nijmegen June 2002. Technical Report NIII-R0204"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Oliveira M Cavalcanti A (2004) From Circus to JCSP. In: Davies J Schulte W Barnett M (eds) ICFEM 2004 Vol 3308 of LNCS. Springer Heidelberg October 2004 pp 320\u2013340","DOI":"10.1007\/978-3-540-30482-1_29"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268075"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.017"},{"issue":"3","key":"e_1_2_1_2_44_2","first-page":"208","article-title":"Interactive verification environments for object-oriented languages","volume":"5","author":"Poetzsch-Heffter A","year":"1999","journal-title":"J Univ Comput Sci"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Reggio G Astesiano E Choppy C Hussmann H (2000) Analysing UML active classes and associated state machines\u2014a lightweight formal approach. In: Maibaum T (ed) Fundamental approaches to software engineering (FASE 2000) Vol 1783 of LNCS. Springer Heidelberg","DOI":"10.1007\/3-540-46428-X_10"},{"key":"e_1_2_1_2_46_2","unstructured":"Rumbaugh J Jacobson I Booch G (1999) The unified modeling language reference manual. Object Technology Series. Addison-Wesley Reading"},{"key":"e_1_2_1_2_47_2","first-page":"353","volume-title":"A classical mind\u2014essays in honour of C.A.R.","author":"Roscoe AW","year":"1994"},{"key":"e_1_2_1_2_48_2","volume-title":"The theory and practice of concurrency","author":"Roscoe AW","year":"1998"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/978-3-540-39958-2_16","volume-title":"Formal methods for open object-based distributed systems (FMOODS\u201903), Vol 2884 of LNCS.","author":"Rasch H","year":"2003"},{"key":"e_1_2_1_2_50_2","first-page":"67","volume-title":"FMOODS 2005: formal methods for open, object-based distributed systems, Vol 3535 of LNCS.","author":"Rasch H","year":"2005"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Snook C Butler M (2005) UML-B: formal modelling and design aided by UML. ACM Trans Softw Eng Methodol","DOI":"10.1145\/1125808.1125811"},{"key":"e_1_2_1_2_52_2","unstructured":"Scattergood JB (1998) The semantics and implementation of machine-readable CSP. PhD thesis University of Oxford"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Smith G Derrick J (1997) Refinement and verification of concurrent systems specified in Object-Z and CSP. In: Hinchey M Liu S (eds) International conference of formal engineering methods (ICFEM). IEEE pp 293\u2013302","DOI":"10.1109\/ICFEM.1997.630436"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"publisher","DOI":"10.5555\/174837"},{"key":"e_1_2_1_2_55_2","unstructured":"Stoerrle H Hausmann JH (2005) Towards a formal semantics of UML 2.0 activities. In: Software engineering 2005 Vol P-64 of LNI. Gesellschaft fuer Informatik pp 117\u2013128"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Sch\u00e4fer T Knapp A Merz S (2001) Model checking UML state machines and collaborations. In: Stoller SD Visser W (eds) ENTCS Vol 55. Elsevier Amsterdam","DOI":"10.1016\/S1571-0661(04)00262-2"},{"key":"e_1_2_1_2_57_2","unstructured":"Smith G (1992) An object-oriented approach to formal specification. PhD thesis Department of Computer Science University of Queensland St.Lucia 4072 Australia October 1992"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"e_1_2_1_2_59_2","volume-title":"The Z notation: a reference manual, 2nd edn","author":"Spivey JM","year":"1998"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"Selic B Rumbaugh J (1998) Using UML for modeling complex real-time systems. Technical report ObjecTime","DOI":"10.1007\/BFb0057795"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Treharne H Schneider SA (2002) Communicating B machines. In: ZB2002: international conference of Z and B Users Vol 2272 of LNCS. Springer Heidelberg","DOI":"10.1007\/3-540-45648-1_22"},{"key":"e_1_2_1_2_62_2","unstructured":"OMG Unified Modeling Language specification version 1.5 March 2003. http:\/\/www.omg.org"},{"key":"e_1_2_1_2_63_2","unstructured":"OMG Unified Modeling Language: Superstructure version 2.0\u2014final adopted specification August 2003 http:\/\/www.omg.org"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650070026"},{"key":"e_1_2_1_2_65_2","first-page":"334","volume-title":"Fundamental approaches of software engineering (FASE 2000), Vol 1783 of LNCS.","author":"Wehrheim H","year":"2000"},{"key":"e_1_2_1_2_66_2","doi-asserted-by":"crossref","unstructured":"Welch PH (2002) Process oriented design for Java: concurrency for all. In: Computational science\u2014ICCS 2002 Vol 2330 of LNCS. Springer Heidelberg April 2002. Keynote Tutorial pp 687\u2013687","DOI":"10.1007\/3-540-46080-2_72"},{"key":"e_1_2_1_2_67_2","unstructured":"International Organisation for Standardization (2002) Information technology\u2014Z formal specification notation\u2014Syntax type system and semantics 1st edn July 2002. ISO\/IEC 13568:2002 (E) International Standard"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-007-0042-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-007-0042-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-007-0042-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:48:41Z","timestamp":1641484121000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-007-0042-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3]]},"references-count":69,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,3]]}},"alternative-id":["10.1007\/s00165-007-0042-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-007-0042-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,3]]}}}