Skip to main content
SpringerLink
Log in

Linking CSP-OZ with UML and Java: A Case Study

  • Conference paper
Integrated Formal Methods (IFM 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2999))

Included in the following conference series:

Abstract

We describe how CSP-OZ, an integrated formal method combining the process algebra CSP with the specification language Object-Z, can be linked to standard software engineering languages, viz. UML and Java. Our aim is to generate a significant part of the CSP-OZ specification from an initially developed UML model using a UML profile for CSP-OZ, and afterwards transform the formal specification into assertions written in the Java Modelling Language JML complemented by CSP jassda . The intermediate CSP-OZ specification serves to verify correctness of the UML model, and the assertions control at runtime the adherence of a Java implementation to these formal requirements. We explain this approach using the case study of a “holonic manufacturing system” in which coordination of transportation and processing is distributed among stores, machine tools and agents without central control.

This research was partially supported by the DFG project ForMooS (grant Ol/98-3).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ábrahám-Mumm, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: Verification for Java’s reentrant multithreading concept. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 4–20. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Bartetzko, D., Fischer, C., Möller, M., Wehrheim, H.: Jass – Java with Assertions. In: Havelund, K., Roşu, G. (eds.) ENTCS, vol. 55, Elsevier, Amsterdam (2001), http://www.elsevier.nl/locate/entcs/volume55.html

    Google Scholar 

  3. Breunesse, C.-B., Poll, E.: Verifying JML specifications with model fields. In: Workshop on Formal Techniques for Java-like Programs – FTfJP 2003. ETH Zürich, Technical Report 108 (July 2003)

    Google Scholar 

  4. Brörkens, M.: Trace- und Zeit-Zusicherungen beim Programmieren mit Vertrag. Master’s thesis, Univ. of Oldenburg, Dept. of Computing Science (January 2002)

    Google Scholar 

  5. Brörkens, M., Möller, M.: Dynamic Event Generation for Runtime Checking using the JDI. In: Havelund, K., Rosu, G. (eds.) ENTCS, vol. 70, Elsevier, Amsterdam (2002), http://www.elsevier.nl/locate/entcs/volume70.html

    Google Scholar 

  6. 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

    Google Scholar 

  7. 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. 70, Elsevier, Amsterdam (2002)

    Google Scholar 

  8. Drusinsky, D.: The Temporal Rover and the ATG Rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 323–330. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  9. 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)

    Article  Google Scholar 

  10. 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. 1789, p. 417. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  11. Engels, G., Küster, 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. 26 (2001)

    Google Scholar 

  12. 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 

  13. 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)

    Chapter  Google Scholar 

  14. 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–334. Springer, Heidelberg (1999)

    Google Scholar 

  15. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn., June 2000. Addison-Wesley, Reading (2000)

    Google Scholar 

  16. Gullekson, G.: Designing for concurrency and distribution with Rational Rose RealTime. Technical report, Rational Software (2000)

    Google Scholar 

  17. 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)

    Chapter  Google Scholar 

  18. Havelund, K., Rosu, G. (eds.): Monitoring Java Programs with Java Path Explorer. ENTCS, vol. 55. Elsevier, Amsterdam (2001)

    Google Scholar 

  19. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  20. 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)

    Chapter  Google Scholar 

  21. 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. 33, pp. 329–340 (1998)

    Google Scholar 

  22. Kramer, R.: iContract - the Java Design by Contract tool. Technical report, Reliable Systems (1998)

    Google Scholar 

  23. 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)

    Article  Google Scholar 

  24. 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

  25. 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. 2852, pp. 262–284. Springer, Heidelberg (2003) (to appear)

    Chapter  Google Scholar 

  26. 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)

    Chapter  Google Scholar 

  27. Poetzsch-Heffter, A., Meyer, J.: Interactive verification environments for objectoriented languages. Journal of Universal Computer Science 5(3), 208–225 (1999)

    Google Scholar 

  28. Möller, M.: Specifying and Checking Java using CSP. In: Workshop on Formal Techniques for Java-like Programs – FTfJP 2002. Computing Science Department, University of Nijmegen, Technical Report NIII-R0204 (June 2002)

    Google Scholar 

  29. Rasch, H.: Translating UML state machines into CSP. Technical report, Universität Oldenburg (2003)

    Google Scholar 

  30. 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. 2884, pp. 229–243. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  31. Reggio, G., Astesiano, E., Choppy, C., Hussmann, H.: Analysing UML active classes and associated state machines – A lightweight formal approach. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, p. 127. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  32. Roscoe, W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)

    Google Scholar 

  33. Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Object Technology Series. Addison-Wesley, Reading (1999)

    Google Scholar 

  34. Schäfer, T., Knapp, A., Merz, S.: Model Checking UML State Machines and Collaborations. In: Stoller, S.D., Visser, W. (eds.). ENTCS, vol. 55, Elsevier, Amsterdam (2001)

    Google Scholar 

  35. Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object-Oriented Modeling. John Wiley & Sons, Chichester (1994)

    MATH  Google Scholar 

  36. Selic, B., Rumbaugh, J.: Using UML for modeling complex real-time systems. Technical report, ObjecTime (1998)

    Google Scholar 

  37. Snook, C., Butler, M.: Tool-Supported Use of UML for Constructing B Specifications. Technical report, http://www.ecs.soton.ac.uk/~mjb/U2Bpaper2.pdf

  38. OMG Unified Modeling Language specification, version 1.5 (March 2003), http://www.omg.org

  39. 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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Oldenburg, 26111, Oldenburg, Germany

    Michael Möller, Ernst-Rüdiger Olderog, Holger Rasch & Heike Wehrheim

Authors
  1. Michael Möller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ernst-Rüdiger Olderog
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Holger Rasch
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Heike Wehrheim
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, University of Kent, CT2 7NF, Canterbury, Kent, UK

    Eerke A. Boiten

  2. Department of Computing, University of Sheffield, S1 4DP, Sheffield, UK

    John Derrick

  3. School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Australia

    Graeme Smith

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Möller, M., Olderog, ER., Rasch, H., Wehrheim, H. (2004). Linking CSP-OZ with UML and Java: A Case Study. In: Boiten, E.A., Derrick, J., Smith, G. (eds) Integrated Formal Methods. IFM 2004. Lecture Notes in Computer Science, vol 2999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24756-2_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24756-2_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-21377-2

  • Online ISBN: 978-3-540-24756-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation