×

zbMATH — the first resource for mathematics

Integrating a formal method into a software engineering process with UML and Java. (English) Zbl 1141.68024
Summary: 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.
The envisaged application area of our approach is the design of distributed reactive systems. To this end, we propose a specific UML profile 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 verifying properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating contracts for the final implementation. Contracts are written in the Java Modeling Language complemented by \(\text{CSP}_{\text{jassda}}\), 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.

MSC:
68N15 Theory of programming languages
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Bandera; Circus; Eiffel; FDR2; Jass; JML; JPAX; SPIN; Z
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ábrahám-Mumm E, de Boer FS, de Roever W-P, Steffen M (2002) Verification for Java’s reentrant multithreading concept. In: FoSSACS 2002, Vol 2303 of LNCS, Springer, Heidelberg, pp 4–20 · Zbl 1077.68552
[2] 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–244 · Zbl 1057.68639
[3] Bartetzko D, Fischer C, Möller M, Wehrheim H (2001) Jass–Java with Assertions. In: Havelund K, Roşu G (eds) ENTCS, Vol 55. Elsevier http://www.elsevier.nl/locate/entcs/volume55.html
[4] Brookes SD, Hoare CAR, Roscoe AW (1984) A theory of communicating sequential processes. J ACM 31: 560–599 · Zbl 0628.68025 · doi:10.1145/828.833
[5] Brörkens M, Möller 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
[6] Brörkens M (2002) Trace- und Zeit-Zusicherungen beim Programmieren mit Vertrag. Master’s thesis, University of Oldenburg, Department of Computing Science, January 2002
[7] 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
[8] Cavalcanti A, Sampaio A, Woodcock J (2003) A refinement strategy for circus. Formal Aspects Comput 15(2-3): 146–181 · Zbl 1093.68555 · doi:10.1007/s00165-003-0006-5
[9] Derrick J, Boiten EA (2003) Relational concurrent refinement. Formal Aspects Comput 15(2-3): 182–214 · Zbl 1093.68061 · doi:10.1007/s00165-003-0007-4
[10] Davies J, Crichton Ch (2003) Concurrency and refinement in the unified modeling language. Formal Aspects Comput 15(2-3): 118–145 · Zbl 1093.68598 · doi:10.1007/s00165-003-0008-3
[11] Damm W, Harel D (2001) LSCs: Breathing life into message sequence charts. Formal Methods Syst Des 19(1): 45–80 · Zbl 0985.68033 · doi:10.1023/A:1011227529550
[12] 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) · Zbl 1075.68048
[13] 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’2000)
[14] Duke R, Rose G, Smith G (1995) Object-Z: A specification language advocated for the description of standards. Comput Stand Interfaces 17: 511–533 · doi:10.1016/0920-5489(95)00024-O
[15] Drusinsky D (2000) The Temporal Rover and the ATG Rover. In: SPIN Modelchecking and Software Verification, volume 1885 of LNCS, Springer, Heidelberg, pp 323–330 · Zbl 0976.68571
[16] Engels G, Küster 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
[17] Formal Systems (Europe) Ltd. (2003) Failures-divergence refinement: FDR2 user manual, May 2003
[18] 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 ’97), Vol 2. Chapman & Hall, London, pp 423–438
[19] 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 · Zbl 0953.68089
[20] Fischer C, Olderog E-R, Wehrheim H (2001) A CSP view on UML-RT structure diagrams. In: Hussmann H (ed) Fundamental approaches to software engineering (FASE’01), Vol 2029 of LNCS. Springer, Heidelberg, 2001, pp 91–108 · Zbl 0977.68575
[21] Fecher H, Schönborn 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–65
[22] 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–334 · Zbl 0963.68128
[23] Gosling J, Joy B, Steele G, Bracha G (2000) The Java language specification, second edition. Addison-Wesley, Reading
[24] Gullekson G (2000) Designing for concurrency and distribution with Rational Rose RealTime. Technical report, Rational Software
[25] 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 · Zbl 1006.68536
[26] Huisman M, Jacobs B (2000) Java program verification via a Hoare Logic with abrupt termination. In: Maibaum T (ed) Fundamental approaches to software engineering (FASE 2000), Vol 1783 of LNCS. Springer, Heidelberg, pp 284–303
[27] Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Englewood Cliffs · Zbl 0637.68007
[28] Havelund K, Rosu G (2004) Efficient monitoring of safety properties. Softw Tools Technol Transf 6(2): 158–173 · Zbl 02243239 · doi:10.1007/s10009-003-0117-6
[29] Havelund K, Rosu G (2004) An overview of the runtime verification tool java pathexplorer. Formal Methods Syst Des 24(2): 189–215 · Zbl 1073.68549 · doi:10.1023/B:FORM.0000017721.39909.4b
[30] 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–340, Oct. 1998
[31] The Java Modeling Language (JML) home page. http://www.jmlspecs.org/
[32] Kramer R (1998) iContract–the Java Design by Contract tool. Technical report, Reliable Systems
[33] 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
[34] 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’02, Vol 2852 of LNCS. Springer, Heidelberg · Zbl 1075.68009
[35] Leino KRM (2001) Extended static checking: a ten-year perspective. In: Wilhelm R (eds) Informatics–10 years back, 10 years ahead, Vol 2000 of LNCS. Springer, Heidelberg, pp 157–175
[36] 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 · Zbl 0977.68672
[37] Latella D, Majzik I, Massink M (1999) Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects Comput 11: 430–445 · Zbl 0966.68124 · doi:10.1007/s001659970003
[38] OMG model driven architecture. Object Management Group. http://www.omg.org/mda
[39] Meyer B (1997) Object-oriented software construction, 2nd edn. Prentice-Hall, Englewood Cliffs · Zbl 0987.68516
[40] Möller M (2002) Specifying and checking Java using CSP. In: Workshop on formal techniques for java-like programs–FTfJP’2002. Computing Science Department, University of Nijmegen, June 2002. Technical Report NIII-R0204
[41] 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–340
[42] Olderog E-R, Hoare CAR (1986) Specification-oriented semantics for communicating processes. Acta Inform 23: 9–66 · Zbl 0569.68019 · doi:10.1007/BF00268075
[43] Olderog E-R, Wehrheim H (2005) Specification and (property) inheritance in CSP-OZ. Sci Comput Program 55: 227–257 · Zbl 1075.68051 · doi:10.1016/j.scico.2004.05.017
[44] Poetzsch-Heffter A, Meyer J (1999) Interactive verification environments for object-oriented languages. J Univ Comput Sci 5(3): 208–225
[45] Reggio G, Astesiano E, Choppy C, Hussmann H (2000) Analysing UML active classes and associated state machines–a lightweight formal approach. In: Maibaum T (ed) Fundamental approaches to software engineering (FASE 2000), Vol 1783 of LNCS. Springer, Heidelberg
[46] Rumbaugh J, Jacobson I, Booch G (1999) The unified modeling language reference manual. Object Technology Series. Addison-Wesley, Reading
[47] Roscoe AW (1994) Model-checking CSP. In: Roscoe AW (eds) A classical mind–essays in honour of C.A.R. Hoare. Prentice-Hall, Englewood Cliffs, pp 353–378
[48] Roscoe AW (1998) The theory and practice of concurrency. Prentice-Hall, Englewood Cliffs.
[49] Rasch H, Wehrheim H (2003) Checking consistency in UML diagrams: classes and state machines. In: Najm E, Nestmann U, Stevens P (eds) Formal methods for open object-based distributed systems (FMOODS’03), Vol 2884 of LNCS. Springer, Heidelberg, pp 229–243 · Zbl 1253.68096
[50] Rasch H, Wehrheim H (2005) Checking the validity of scenarios in UML models. In: Steffen M, Zavatarro G (eds) FMOODS 2005: formal methods for open, object-based distributed systems, Vol 3535 of LNCS. Springer, Heidelberg, pp 67–82
[51] Snook C, Butler M (2005) UML-B: formal modelling and design aided by UML. ACM Trans Softw Eng Methodol
[52] Scattergood JB (1998) The semantics and implementation of machine-readable CSP. PhD thesis, University of Oxford
[53] 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–302
[54] Selic B, Gullekson G, Ward PT (1994) Real-time object-oriented modeling. Wiley, New York. · Zbl 0821.68128
[55] 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–128
[56] Schäfer T, Knapp A, Merz S (2001) Model checking UML state machines and collaborations. In: Stoller SD, Visser W (eds) ENTCS, Vol 55. Elsevier, Amsterdam
[57] 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
[58] Smith G (2000) The object-Z specification language. Kluwer, Dordrecht. · Zbl 0944.68124
[59] Spivey JM (1998) The Z notation: a reference manual, 2nd edn. Prentice-Hall, Oxford.
[60] Selic B, Rumbaugh J (1998) Using UML for modeling complex real-time systems. Technical report, ObjecTime
[61] Treharne H, Schneider SA (2002) Communicating B machines. In: ZB2002: international conference of Z and B Users, Vol 2272 of LNCS. Springer, Heidelberg · Zbl 1044.68121
[62] OMG Unified Modeling Language specification, version 1.5, March 2003. http://www.omg.org
[63] OMG Unified Modeling Language: Superstructure, version 2.0–final adopted specification, August 2003 http://www.omg.org
[64] Wehrheim H (2000) Data abstraction techniques in the validation of CSP-OZ specifications. Formal Aspects Comput 12: 147–164 · Zbl 0966.68125 · doi:10.1007/s001650070026
[65] Wehrheim H (2000) Specification of an automatic manufacturing system – a case study in using integrated formal methods. In: Maibaum T (eds) Fundamental approaches of software engineering (FASE 2000), Vol 1783 of LNCS. Springer, Heidelberg, pp 334–348
[66] Welch PH (2002) Process oriented design for Java: concurrency for all. In: Computational science–ICCS 2002, Vol 2330 of LNCS. Springer, Heidelberg, April 2002. Keynote Tutorial, pp 687–687 · Zbl 1055.68517
[67] International Organisation for Standardization (2002) Information technology–Z formal specification notation–Syntax, type system and semantics, 1st edn, July 2002. ISO/IEC 13568:2002 (E) International Standard
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.