Abstract
This paper presents an approach and a tool to increase specification quality by using a combination of UML and formal languages. Our approach is based on the expression of the UML class diagram and its annotations into a Z formal specification. Our tool called RoZ supports this approach by making the transition between the UML world and the Z world : from an annotated class diagram, it automatically generates a complete Z specification, the specifications of some elementary operations and some proof obligations to validate the model constraints.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
J. Brunet. An enhanced definition of composition and its use for abstraction. The 5th international conference on Object Oriented Information Systems, Paris, September 1998.
Rational Software Corporation. UNIFIED MODELING LANGUAGE — notation guide version 1.1. September 1997.
Y. Ou. On Using UML Class Diagram for Object-Oriented Database Design — Specification of Integrity Constraints. Proc “UML”’ 98 Beyong the Notation, Mulhouse, France, June 1998.
J. Warmer and A. Kleppe. The Object Constraints Language. Addison-Wesley, 1998.
J.M. Spivey. The Z notation — a reference manual (second edition). Prentice-Hall International, 1992.
M. Saaltink. The Z/EVES system. In j. Bowen, M. Hinchey and D. Till editors, Proc. 10th Int. Conf. On the Z formal method (ZUM), volume 1212 of Lecture Notes in Computer Science, pages 72–88, Reading, UK, April 1997.
Rational Software Corporation. Rational Rose — Using Rational Rose 4.0. 1996.
Rational Software Corporation. Rational Rose — Using Rational Rose 98. 1998.
R. France and JM. Bruel and M. Larrondo-Petrie and M. Shroff. Exploring the Semantics of UML type structures with Z. Proc. 2nd IFIP Workshop on Formal Methods for Open Object-Based Distributed Systems (FMOODS), 1997.
M. Shroff and R.B. France. Towards a Formalization of UML class structures in Z. COMPSAC’97, 1997.
K. Lano, H. Houghton, P. Wheeler. Integrating Formal and Structured Methods in Object-Oriented System Development. In Formal Methods and Object technology, Chapter 7, Springer, 1996.
P. Facon, R. Laleau Laleau and H.P. Nguyen. Mapping Object Diagrams into B Specifications. Proc of the Method Integration Workshop, Springer-Verlag, Leeds, March 1996.
S. Dupuy, Y. Ledru and M. Chabre-Peccoud. Vers une intégration utile de notations semiformelles et formelles: un expérience en UML et Z. revue l’Objet, numéro spécial sur les méthodes formelles pour les systèmes à objets, 2000, to appear.
S. Dupuy. RoZ version 0.3 an environment for the integration of UML and Z. technical report Laboratoire LSR-IMAG, 1999. http://www-lsr.imag.fr/Les.Groupes/PFL/RoZ/index.html
Y. Ledru. Identifying pre-conditions with the Z/EVES theorem prover. Proc Int. IEEE Conference on Automated Software Engineering’98, IEEE Computer Society Press, October 1998.
Y. Ledru. Complementing semi-formal specifications with Z. KBSE’96, IEEE Computer Society Press, 1996.
N. Hadj-Rabia and H. Habrias. Formal specification from NIAM model: a Bottom-Up Approach. ISCIS XI (11th int. Symposium on Computer and Information Sciences), Antalya, Turkey, November 1996.
H.P. Nguyen. Dérivation de Spécifications Formelles B à Partir de Spécifications Semi-Formelles. PhD thesis, CNAM, December 1998.
B. Nuseibeh and A. Finkelstein. ViewPoints: a vehicle for method and tool integration. IEEE Proc. Of the 5th Int. Workshop on CASE (CASE’92), p50–60, Montreal, Canada, July 1992.
R. Laleau, N. Nadj-Rabia. Génération automatique de spécifications VDM à partir d’un schéma conceptuel de données. Dans Actes du 13ème congrès INFORSID, Grenoble, France, June 1995.
J.C. Freire Junior, M. Chabre-Peccoud, A. Front and J.-P. Giraudin. A CASE Tool for modeling of methods and information systems. OOIS’98, Int. Conference on Object-Oriented Information Systems, Springer, Paris, France, September 1998.
IFAD. the Rose-VDM++ Link. http://www.ifad.dk/Products/rose-vdmpp.htm
Headway Software. RoZeLink 1.0. http://www.calgary.shaw.wave.ca./headway/index.htm
R.B. France, J.-M. Bruel, M.M. Larrondo-Petrie. An Integrated Object-Oriented and Formal Modeling Environment. Journal of Object Oriented Programming, November/December 1997.
P. Caspi, N. Halbwachs, D. Pilaud and J. Plaice. LUSTRE, a declarative language for programming synchronous systems. In 14th Symposium on Principles of Programming Languages (POPL’87), ACM, p 178–188, Munich, 1987.
G. Booch, I. Jacobson and J. Rumbaugh. The Unified Modeling Language-User Guide. Addison-Wesley, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dupuy, S., Ledru, Y., Chabre-Peccoud, M. (2000). An Overview of RoZ : A Tool for Integrating UML and Z Specifications. In: Wangler, B., Bergman, L. (eds) Advanced Information Systems Engineering. CAiSE 2000. Lecture Notes in Computer Science, vol 1789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45140-4_28
Download citation
DOI: https://doi.org/10.1007/3-540-45140-4_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67630-0
Online ISBN: 978-3-540-45140-2
eBook Packages: Springer Book Archive