Abstract
Object models and formal notations offer complementary advantages for information systems analysis and design. In this paper, we consider the mapping of OMT notations into Object-Z formal specifications for the OMT dynamic model. This allows to better specify the OMT semantics and some of the consistency rules between the object model and the dynamic one. We propose a constructive way to develop a formal specification. Our work develops a systematic translation process in order to produce formal specifications with good readability and traceability quality. Such proposals should help to implement CASEs integrating multi-modelling processes (natural, graphical, formal) producing better system specifications tools.
This work was partially funded by the Rhône-Alpes region through the Emergence programme
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Buessow, R., Weber, M.: BW: A steam-boiler control specification with Statecharts and Z. In: Abrial, J.-R., Börger, E., Langmaack, H. (eds.) Dagstuhl Seminar 1995. LNCS, vol. 1165, pp. 109–128. Springer, Heidelberg (1996)
Duke, R., Kin, P., Rose, G., Smith, G.: The Object-Z specification langage: Version 1. Technical Report 91-1, Software Verification Research Centre, Department of Computer Science, University of Queensland, Australia (April 1991)
Dupuy, S., Ledru, Y., Chabre-Peccoud, M.: Integrating OMT and Object-Z. In: Evans, A., Lano, K. (eds.) Proc. BCS FACS/EROS ROOM Workshop, London, UK, Department of Computing, Imperial College. Technical Report GR/K67311-2 (June 1997)
Wand, E., Richter, H., Cheng, B.: Formalizing and integrating the dynamic model within OMT. In: Proc. 19th International Conference on Software Engineering, Boston, USA (May 1997)
Facon, P., Laleau, R., Nguyen, H.P.: Dérivation de spécifications formelles B à partir de spécifications semi-formelles de systèmes d’information. In: Habrias, H. (ed.) Proc. 1st Conference on the B Method, Nantes, France (November 1996)
Facon, P., Laleau, R., Nguyen, H.P.: Mapping object diagrams into B specifications. In: Bryant, A., Semmens, L. (eds.) Method Integration Workshop, Electronic Workshops in Computing. Springer, Heidelberg (1996)
France, R., Bruel, J.-M.: Using formal techniques to strengthen informal objectoriented modeling techniques: The FuZE experience. Technical report, Department of Computer Science and Engineering, Florida Atlantic University, Boca Raton, USA (1997)
France, R., Bruel, J.-M., Larrondo-Petrie, M., Shroff, M.: Exploring the semantics of UML type structures with Z. In: Bowman, H., Derrick, J. (eds.) Proc. 2nd IFIP Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), pp. 247–260. Chapman and Hall, Boca Raton (1997)
Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)
Lano, K.: Formal Object-Oriented Development. FACIT. Springer, Heidelberg (1995)
Lano, K., Goldsack, S.: Integrated formal and object-oriented methods: The VDM++ approach. In: Bryant, A., Semmens, L. (eds.) Method Integration Workshop, Electronic Workshops in Computing, Springer, Heidelberg (1996)
Lano, K., Houghton, H., Wheeler, P.: Integrating Formal and Structured Methods in Object-Oriented System Development, ch. 7. Springer, Heidelberg (1996)
Polack, F., Whiston, M., Mander, K.: The SAZ project: Integrating SSADM and Z. In: Larsen, P.G., Woodcock, J.C.P. (eds.) FME 1993. LNCS, vol. 670, pp. 541–557. Springer, Heidelberg (1993)
Randell, G.P.: Translating data flow diagrams into Z (and vice versa). Technical Report 90019, Royal Signals and Radar Establishement, Malvern, UK (October 1990)
Rumbaugh, J., Blaha, M., Premerlani, M., Eddy, F., Lorensen, W.: Object- Oriented Modeling and Design. Prentice Hall International, Englewood Cliffs (1991)
Saiedian, H.: An invitation to formal methods. IEEE Computer 24(4), 16–30 (1996)
The UML Group. UML Notation Guide, Version 1.1 366 (September 1997), http://www.rational.com/uml/documentation.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dupuy, S., Ledru, Y., Chabre-Peccoud, M. (1998). Translating the OMT Dynamic Model into Object-Z. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds) ZUM ’98: The Z Formal Specification Notation. ZUM 1998. Lecture Notes in Computer Science, vol 1493. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49676-2_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-49676-2_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65070-6
Online ISBN: 978-3-540-49676-2
eBook Packages: Springer Book Archive