Abstract
This paper presents a systematic transformation of semi-formal specifications expressed with OMT notations into formal specifications. The object model is first transformed into a specification composed of a set of B machines. Then each component of the dynamic model is transformed and integrated into the previous specification leading to a single specification. Transformations are presented as generic templates. When using these templates, the generated specification is automatically proved within the B prover relatively to the invariant preservation.
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.R. Abrial. Extending B without Changing it (for Developing Distributed Systems). In H. Habrias, editor, Putting Into Practice Methods and Tools for Information System Design-1st Conference on the B Method, Nantes (F), November 1996.
J.R. Abrial. The B Book-Assigning Programs to Meanings. Cambridge University Press, 1996. ISBN 0-521-49619-5.
J.R. Abrial and L. Mussat. Introducing Dynamic Constraints in B. In D. Bert, editor, B’98: Recent Advances in the Development and Use of the B Method-2nd International B Conference, number 1393 in Lecture Notes in Computer Science, Montpellier (F), April 1998. Springer-Verlag.
D. Coleman, P. Arnold, St. Bodo, Ch. Dollin, H. Gilchrist, F. Hayes, and P. Jeremaes. Object-Oriented Development: The Fusion Method. Prentice Hall, 1994.
S. Dupuy, Y. Ledru, and M. Chabre-Peccoud. Integrating OMT and Object-Z. In BCS FACS/EROS ROOM Workshop, London (UK), June 1997.
S. Dupuy, Y. Ledru, and M. Chabre-Peccoud. Translating the OMT Dynamic Model into Object-Z*. In ZUM’98: The Z Formal Specification Notation-11th International Conference of Z Users, number 1493 in Lecture Notes in Computer Science, Berlin (D), September 1998.
P. Facon and R. Laleau. Des modèles d’objets aux spécifications formelles ensemblistes. Revue Ingénierie des Systèmes d’Information, 4(2), 1996.
P. Facon, R. Laleau, and H.P. Nguyen. Dérivation de spécifications formelles B àpartir de spécifications semi-formelles de systèmes d’information. In H. Habrias, editor, Putting Into Practice Methods and Tools for Information System Design-1st Conference on the B Method, Nantes (F), November 1996.
P. Facon, R. Laleau, and H.P. Nguyen. Mapping Object Diagrams into B Specications. In A. Bryant and L. Semmens, editors, Methods Integration Workshop, Electronic Workshops in Computing (eWiC), Leeds (UK), March 1996. Springer-Verlag.
K. Lano. The B Language and Method: A Guide to Practical Formal Development. FACIT. Springer-Verlag, 1996. ISBN 3-540-76033-4. 894 Eric Meyer and Jeanine Souqui_eres
K. Lano, H. Haughton, and P. Wheeler. Formal Methods and Object Technology, chapter Integrating Formal and Structured Methods in Object-Oriented System Development, pages 113–157. FACIT. Springer-Verlag, 1996. S.J. Goldsack and S.J.H. Kent eds.
N. Lévy and J. Souquières. Modelling Specification Construction by Successive Approximations. In M. Johnson, editor, 6th International AMAST Conference, pages 351–364, Sydney (A), 1997. Springer Verlag 1349.
N. Nagui-Raiss. A formal Software Specification Tool Using The Entity-Relationship Model. In 13th International Conference on the Entity-Relationship Approach, number 881 in Lecture Notes in Computer Science, Manchester (UK), December 1994. Springer-Verlag.
F. Polack, M. Whiston, and K. Pronk. The SAZ Project: Integration SSADM and Z. In International Symposium Formal Methods Europe, number 670 in Lecture Notes in Computer Science, Odense (DK), April 1993. Springer-Verlag.
J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, and W. Lorensen. Object-Oriented Modeling and Design. Prentice Hall Inc. Englewood Cliffs, 1991.
J. Rumbaugh, I. Jacobson, and G. Booch. The United Modeling Language Reference Guide. Addison-Wesley, 1998. ISBN 020130998X.
E. Sekerinski. Graphical Design of Reactive Systems. In D. Bert, editor, B’98:Recent Advances in the Development and Use of the B Method-2nd International B Conference, number 1393 in Lecture Notes in Computer Science, Montpellier(F), April 1998. Springer-Verlag.
R. Shore. An Object-Oriented Approach to B. In H. Habrias, editor, Putting Into Practice Methods and Tools for Information System Design-1st Conference on the B Method, Nantes (F), November 1996.
STERIA-Technologies de l’Information, Aix-en-Provence (F). Atelier B, Manuel Utilisateur, 1998. Version 3.5.
E. Wand, H. Richter, and B. Cheng. Formalizing and integrating the dynamic model within OMT. In 19th International Conference on Software Engineering, Boston (USA), July 1997.
P.T. Ward. How to Integrate Object Orientation with Structured Analysis and Design. In IEEE Software. March 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meyer, E., Souquières, J. (1999). A Systematic Approach to Transform OMT Diagrams to a B Specification. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1708. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48119-2_48
Download citation
DOI: https://doi.org/10.1007/3-540-48119-2_48
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66587-8
Online ISBN: 978-3-540-48119-5
eBook Packages: Springer Book Archive