{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:33:24Z","timestamp":1725489204760},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540417910"},{"type":"electronic","value":"9783540452515"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45251-6_14","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T05:53:28Z","timestamp":1186898008000},"page":"242-258","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Validation of UML Models Thanks to Z and Lustre"],"prefix":"10.1007","author":[{"given":"Sophie","family":"Dupuy-Chessa","sequence":"first","affiliation":[]},{"given":"Lydie","family":"du Bousquet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,16]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"J.R. Abrial. The B-Book. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"14_CR2","unstructured":"D.J. Andrews, H. Bruun, B.S. Hansen, P.G. Larsen, N. Plat, et al. Information Technology \u2014 Programming Languages, their environments and system software interfaces-Vienna Development Method-Specification Language Part 1: Base language. ISO, 1995."},{"key":"14_CR3","unstructured":"G. Booch, I. Jacobson, and J. Rumbaugh. The Unified Modeling Language-User Guide. Addison-Wesley, 1998."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"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), Munich, pages 178\u2013188. ACM Press, 1987.","DOI":"10.1145\/41625.41641"},{"key":"14_CR5","volume-title":"Workshop on Industrial-Strength Formal Specification Techniques","author":"J. Crow","year":"1995","unstructured":"J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas. A tutorial introduction to PVS. In Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, USA, April 1995."},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"L. du Bousquet, F. Ouabdesselam, J.-L. Richier, and N. Zuanon. Lutess: a specification-driven testing environment for synchronous software. In 21st International Conference on Software Engineering, pages 267\u2013276. ACM Press, May 1999.","DOI":"10.1007\/978-3-7091-6355-9_4"},{"key":"14_CR7","series-title":"PhD thesis","volume-title":"Couplage de notations semi-formelles et formelles pour la sp\u00e9cification des Syst\u00e9mes d\u2019Informations","author":"S. Dupuy","year":"2000","unstructured":"S. Dupuy. Couplage de notations semi-formelles et formelles pour la sp\u00e9cification des Syst\u00e9mes d\u2019Informations. PhD thesis, Universit\u00e9 Joseph Fourier, Grenoble, 2000."},{"key":"14_CR8","series-title":"technical report PFL","volume-title":"Cash-Point service\u201d: a multi-formalism approach for specification","author":"S. Dupuy","year":"1999","unstructured":"S. Dupuy and L. du Bousquet. \u201cCash-Point service\u201d: a multi-formalism approach for specification. technical report PFL, IMAG-LSR, Grenoble, France, 1999."},{"key":"14_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45140-4_28","volume-title":"12th Conference on Advanced information Systems Engineering-CAiSE\u20192000","author":"S. Dupuy","year":"2000","unstructured":"S. Dupuy, Y. Ledru, and M. Chabre-Peccoud. An Overview of RoZ: a Tool for Integrating UML and Z Specifications. In 12th Conference on Advanced information Systems Engineering-CAiSE\u20192000, volume 1789 of Lecture Notes in Computer Science, Stockholm, Sweden, 2000. Springer-Verlag."},{"key":"14_CR10","unstructured":"S. Dupuy, Y. Ledru, and M. Chabre-Peccoud. Vers une int\u00e9gration utile de notations semiformelles et formelles: une exp\u00e9rience en UMLetZ. L\u2019Objet, num\u00e9ro th\u00e9matique M\u00e9thodes formelles pour les objets, 6(1), 2000."},{"key":"14_CR11","unstructured":"R. France, J.-M. Bruel, and M. Larrondo-Petri. An Integrated Object-Oriented and Formal Modeling Environment. Journal of Object Oriented Programming, pages 25\u201334, November\/Decembrer 1997."},{"key":"14_CR12","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/978-0-387-35261-9_17","volume-title":"Proc. 2nd IFIP Workshop on Formal Methods for Open Object-Based Distributed Systems (FMOODS)","author":"R. France","year":"1997","unstructured":"R. France, J.-M. Bruel, M. Larrondo-Petrie, and M. Shroff. Exploring the Semantics of UML type structures with Z. In H. Bowman and J. Derrick, editors, Proc. 2nd IFIP Workshop on Formal Methods for Open Object-Based Distributed Systems (FMOODS), pages 247\u2013260, Canterbury, UK, 1997. Chapman and Hall, London."},{"key":"14_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054165","volume-title":"Proceedings of the First Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"H. Garavel","year":"1998","unstructured":"Hubert Garavel. Open\/c\u00e6sar: An open software architecture for verification, simulation, and testing. In Proceedings of the First Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS 1384, Springer Verlag, 1998."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, F. Lagnier, and C. Ratel. Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Programming Language LUSTRE. IEEE Transactions on Software Engineering, pages 785\u2013793, September 1992.","DOI":"10.1109\/32.159839"},{"issue":"3","key":"14_CR15","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231\u2013274, 1987.","journal-title":"Science of Computer Programming"},{"key":"14_CR16","unstructured":"W.-M. Ho, J.-M. J\u00e9z\u00e9quel, A. LeGuennec, and F. Pennaneac\u2019h. Umlaut: an extensible uml transformation framework. In Proceedings of Automated Software Engineering (ASE), Florida, USA, October 1999. IEEE."},{"key":"14_CR17","unstructured":"IFAD. The Rose-VDM++ Link. http:\/\/www.ifad.dk\/Products\/rose-vdmpp.htm ."},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"K Lano and S. Goldsack. Intregrated Formal and Object-Oriented Methods: The VDM++ Approach. In A. Bryant and L. Semmens, editors, Proceedings of Method Integration Workshop, Electronic Workshop in Computing, Leeds, March 1996. Springer-Verlag.","DOI":"10.14236\/ewic\/MI1996.10"},{"key":"14_CR19","unstructured":"Y. Ledru. Identifying pre-conditions with the Z\/EVES theorem prover. In Proc. of the 13th Int. Conf. on Automated Software Engineering. IEEE, 1998."},{"key":"14_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"875","DOI":"10.1007\/3-540-48119-2_48","volume-title":"World Congress on Formal Methods in the Development of Computing Systems-FM\u201999","author":"E. Meyer","year":"1999","unstructured":"E. Meyer and J. Souqui\u00e8res. A systematic approach to transform OMT diagrams to a B specification. In J. Wing, J. Woodcock, and J. Davies, editors, World Congress on Formal Methods in the Development of Computing Systems-FM\u201999, volume 1708of Lecture Notes in Computer Science, pages 875\u2013896, Toulouse, France, 1999. Springer-Verlag."},{"key":"14_CR21","unstructured":"F. Polack, M. Whiston, and K. Mander. The SAZ Project: Integrating SSADM and Z. In International Symposium Formal Methods Europe, Odense, Danemark, Avril 1993."},{"key":"14_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/BFb0027284","volume-title":"The Z\/EVES system","author":"M. Saaltink","year":"1997","unstructured":"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\u201388, Reading, UK, april 1997. Springer-Verlag, Berlin."},{"key":"14_CR23","unstructured":"Headway Software. The RoZeLink 1.0. http:\/\/www.calgary.shaw.wave.ca\/headway\/index.htm ."},{"key":"14_CR24","unstructured":"J.M. Spivey. The Z notation. Prentice-Hall International, 1992."},{"key":"14_CR25","unstructured":"J. Warmer and A. Kleppe. The Object Constraint Language. Addison-Wesley, 1998."}],"container-title":["Lecture Notes in Computer Science","FME 2001: Formal Methods for Increasing Software Productivity"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45251-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T20:23:00Z","timestamp":1587846180000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45251-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417910","9783540452515"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-45251-6_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"16 March 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}