{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,12]],"date-time":"2024-12-12T05:44:10Z","timestamp":1733982250691,"version":"3.30.2"},"reference-count":36,"publisher":"Elsevier BV","issue":"7","license":[{"start":{"date-parts":[[2003,10,1]],"date-time":"2003-10-01T00:00:00Z","timestamp":1064966400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information Systems"],"published-print":{"date-parts":[[2003,10]]},"DOI":"10.1016\/s0306-4379(02)00081-9","type":"journal-article","created":{"date-parts":[[2003,3,4]],"date-time":"2003-03-04T15:38:35Z","timestamp":1046792315000},"page":"753-768","source":"Crossref","is-referenced-by-count":1,"title":["Visualizing graphical and textual formalisms"],"prefix":"10.1016","volume":"28","author":[{"given":"R","family":"Castello","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R","family":"Mili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0306-4379(02)00081-9_BIB1","unstructured":"G. Berry, A quick guide to ESTEREL version 5.10, release 1.0, Technical report, Ecole des Mines and INRIA, February 1997."},{"year":"1991","series-title":"Design and Validation of Computer Protocols","author":"Holzmann","key":"10.1016\/S0306-4379(02)00081-9_BIB2"},{"issue":"5","key":"10.1016\/S0306-4379(02)00081-9_BIB3","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker spin","volume":"23","author":"Holzmann","year":"1997","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB4","doi-asserted-by":"crossref","unstructured":"F. Maraninchi, N. Halbwachs, Compiling ARGOS into Boolean equations, in: Lecture Notes in Computer Science, Vol. 1135, Springer, Berlin, 1996, pp. 72\u201390.","DOI":"10.1007\/3-540-61648-9_35"},{"key":"10.1016\/S0306-4379(02)00081-9_BIB5","doi-asserted-by":"crossref","unstructured":"A. Benveniste, P.L. Guernic, C. Jacquemot, Synchronous programming with events and relations: the SIGNAL language an its semantics, Sci. Comput. Programming (16) (1991) 103\u2013149.","DOI":"10.1016\/0167-6423(91)90001-E"},{"year":"1989","series-title":"The Z Notation, A reference Manual","author":"Spivey","key":"10.1016\/S0306-4379(02)00081-9_BIB6"},{"year":"1991","series-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Manna","key":"10.1016\/S0306-4379(02)00081-9_BIB7"},{"issue":"3","key":"10.1016\/S0306-4379(02)00081-9_BIB8","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","article-title":"Statecharts","volume":"8","author":"Hare","year":"1987","journal-title":"Sci. Comput. Programming"},{"issue":"3","key":"10.1016\/S0306-4379(02)00081-9_BIB9","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1145\/356698.356702","article-title":"Petri nets","volume":"9","author":"Peterson","year":"1977","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB10","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/S0164-1212(01)00137-6","article-title":"Vista: a tool suite for the visualization of behavioral requirements","volume":"62","author":"Castell\u00f3","year":"2002","journal-title":"Journal of Systems and Software"},{"key":"10.1016\/S0306-4379(02)00081-9_BIB11","unstructured":"R. Castell\u00f3, From informal specification to formalization: an automated visualization approach, Ph.D. Thesis, The University of Texas at Dallas, 2000."},{"issue":"4","key":"10.1016\/S0306-4379(02)00081-9_BIB12","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/235321.235322","article-title":"The STATEMATE semantics of statecharts","volume":"5","author":"Harel","year":"1996","journal-title":"ACM Trans. Software Eng. Meth."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB13","unstructured":"A.S. Tools, Real-time studio: the rational alternative, Available from Artisan Software Tools over the Internet, http:\/\/www.artisansw.com\/rtdialogue\/pdfs\/rational.pdf. Accessed on April 1999."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB14","unstructured":"Rational Rose java, Downloaded from Rational over the Internet, http:\/\/www.rational.com. Accessed on November 1999."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB15","unstructured":"R. O'Donnel, B. Waldt, J. Bergstrand, Automatic code for embedded systems based on formal methods, Available from Telelogic over the Internet, http:\/\/www.Telelogic.se\/solution\/techpap.asp. Accessed on April 1999."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB16","unstructured":"B27 traffic control system, Available over the Internet, http:\/\/www.csr.ncl.ac.uk\/projects\/FME\/InfRes\/applications\/fmadb015.html. Accessed on June 2000."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB17","unstructured":"Bmw rolls-royce system test facility (stf), Available over the Internet, http:\/\/www.csr.ncl.ac.uk\/projects\/FME\/InfRes\/applications\/fmadb018.html. Accessed on June 2000."},{"issue":"2","key":"10.1016\/S0306-4379(02)00081-9_BIB18","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1109\/32.345826","article-title":"Specifying a safety-critical control system in Z","volume":"21","author":"Jacky","year":"1995","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB19","series-title":"FME\u201996: Industrial Benefit and Advances in Formal Methods","first-page":"105","article-title":"Integrating action systems and Z in a medical system specification","volume":"Vol. 1051","author":"Kasurinen","year":"1996"},{"key":"10.1016\/S0306-4379(02)00081-9_BIB20","doi-asserted-by":"crossref","unstructured":"L. Lamport, TLZ in: J.P. Bowen, J.A. Hall (Eds.), Workshops in Computing, Springer, Berlin, 1994, pp. 267\u2013268 Z user Workshop, Cambridge, UK, June 1994, in: Proceedings.","DOI":"10.1007\/978-1-4471-3452-7_15"},{"key":"10.1016\/S0306-4379(02)00081-9_BIB21","series-title":"ZUM\u201997: The Z Formal Specification Notation","first-page":"275","article-title":"An improved recipe for specifying reactive systems in Z","volume":"Vol. 1212","author":"Evans","year":"1997"},{"key":"10.1016\/S0306-4379(02)00081-9_BIB22","series-title":"ZUM\u201998: The Z Formal Specification Notation","first-page":"136","article-title":"Analyzing a real-time program with Z","volume":"Vol. 1493","author":"Jacky","year":"1998"},{"key":"10.1016\/S0306-4379(02)00081-9_BIB23","unstructured":"Hol-Z, Available over the Internet, http:\/\/www.first.gmd.de\/santen\/HOL-Z\/, Accessed on June 2000."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB24","unstructured":"Proofpower, Available over the Internet, http:\/\/www.lemma-one.demon.co.uk\/ProofPower\/, Accessed on June 2000."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB25","unstructured":"Mathias, Mathematics in Animation Suite, Available from Dr Ron Knott's Web site over the Internet. http:\/\/web.comlab.ox.ac.uk\/oucl\/software\/fuzz.html, Accessed on June 2000."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB26","unstructured":"Possum, Available over the Internet, http:\/\/svrc.it.uq.edu.au\/Possum\/, Accessed on June 2000."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB27","unstructured":"J.M. Spivey, FuZZ type checker, Available from The Spivey Partnership over the Internet, http:\/\/web.comlab.ox.ac.uk\/oucl\/software\/fuzz.html, Accessed on June 2000."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB28","unstructured":"The SMV Model Checker, Available over the Internet, http:\/\/www.cs.cmu.edu\/modelcheck\/smv.html, Accessed on July 2000."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB29","unstructured":"Zeta, Available over the Internet, http:\/\/uebb.cs.tu-berlin.de\/zeta\/, Accessed on June 2000."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB30","series-title":"Graph Drawing (Proceedings GD\u201997)","first-page":"248","article-title":"Which aesthetic has the greatest effect on human understanding","volume":"Vol. 1353","author":"Purchase","year":"1997"},{"key":"10.1016\/S0306-4379(02)00081-9_BIB31","doi-asserted-by":"crossref","unstructured":"R. Castell\u00f3, R. Mili, I.G. Tollis, Automatic layout of statecharts, Software Practice and Experience, Wiley, 32, 2002, pp. 25\u201355.","DOI":"10.1002\/spe.418"},{"key":"10.1016\/S0306-4379(02)00081-9_BIB32","unstructured":"Z\/eves, Available over the Internet, http:\/\/www.ora.on.ca\/z-eves\/, Accessed on August 2000."},{"issue":"2","key":"10.1016\/S0306-4379(02)00081-9_BIB33","first-page":"62","article-title":"Temporal logic and Z specifications","volume":"21","author":"Duke","year":"1989","journal-title":"Australian Computer Journal"},{"key":"10.1016\/S0306-4379(02)00081-9_BIB34","doi-asserted-by":"crossref","unstructured":"J. Beauvais, T. Gautier, P.L. Guernic, R. Houdebine, E. Rutten, A translation of statecharts into signal, in: Proceedings of the International Conference on Application of Concurrency to System Design, Aizu-Wakamatsu, Japan, 1998, pp. 52\u201362.","DOI":"10.1109\/CSD.1998.657539"},{"key":"10.1016\/S0306-4379(02)00081-9_BIB35","unstructured":"E. Mikk, Y. Lakhnech, M. Siegel, Implementing statecharts in PROMELA\/SPIN, in: Proceedings of the Second IEEE Workshop on Industrial Strength Formal Specification Techniques, Boca Raton, FL, 1998, pp. 90\u2013101."},{"key":"10.1016\/S0306-4379(02)00081-9_BIB36","series-title":"FM\u201999\u2014Formal Methods","first-page":"987","article-title":"A translation of statecharts to esterel","volume":"Vol. 1709","author":"Seshia","year":"1999"}],"container-title":["Information Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0306437902000819?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0306437902000819?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,30]],"date-time":"2019-03-30T14:27:44Z","timestamp":1553956064000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0306437902000819"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,10]]},"references-count":36,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2003,10]]}},"alternative-id":["S0306437902000819"],"URL":"https:\/\/doi.org\/10.1016\/s0306-4379(02)00081-9","relation":{},"ISSN":["0306-4379"],"issn-type":[{"type":"print","value":"0306-4379"}],"subject":[],"published":{"date-parts":[[2003,10]]}}}