{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:04Z","timestamp":1725484264134},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540437031"},{"type":"electronic","value":"9783540478843"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-47884-1_10","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T20:46:26Z","timestamp":1179607586000},"page":"165-184","source":"Crossref","is-referenced-by-count":5,"title":["Model Checking Object-Z Using ASM"],"prefix":"10.1007","author":[{"given":"Kirsten","family":"Winter","sequence":"first","affiliation":[]},{"given":"Roger","family":"Duke","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,4,23]]},"reference":[{"key":"10_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46419-0_23","volume-title":"Proc. of 6th Int. Conference for Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2000)","author":"G. Castillo Del","year":"2000","unstructured":"G. Del Castillo and K. Winter. Model checking support for the ASM high-level language. In S. Graf and M. Schwartzbach, editors, Proc. of 6th Int. Conference for Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2000), vol. 1785 of LNCS, Springer-Verlag, 2000."},{"key":"10_CR2","volume-title":"PhD thesis","author":"G. Castillo Del","year":"2000","unstructured":"G. Del Castillo. The ASM Workbench. PhD thesis, Department of Mathematics and Computer Science of Paderborn University, Germany, 2000."},{"key":"10_CR3","unstructured":"R. Duke and G. Rose. Formal Object-Oriented Specification Using Object-Z. Macmillan Press, 2000."},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 996\u20131072. Elsevier Science Publishers, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"C. Fischer and H. Wehrheim. Model-checking CSP-OZ specifications with FDR. In K. Araki, A. Galloway and K. Taguchi editors, Proceedings of the 1st International Conference on Integrated Formal Methods (IFM\u201999), pages 315\u2013334. Springer-Verlag, 1999.","DOI":"10.1007\/978-1-4471-0851-1_17"},{"key":"10_CR6","unstructured":"Formal Systems (Europe) Ltd. Failures-Divergence Refinement: FDR2 User Manual, Oct 1997."},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"W. Grieskamp. A computation model for Z based on concurrent constraint resolution. In ZB2000-International Conference of Z and B Users, September, 2000.","DOI":"10.1007\/3-540-44525-0_24"},{"key":"10_CR8","unstructured":"Y. Gurevich. May 1997 Draft of the ASM Guide. Technical report, University of Michigan EECS Department, 1997."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Y. Gurevich. Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic, 2000.","DOI":"10.1145\/343369.343384"},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"981","DOI":"10.1016\/0169-7552(93)90095-L","volume":"XXV","author":"G. Holzmann","year":"1993","unstructured":"G. Holzmann. Design and validation of protocols: A tutorial. In Computer Networks and ISDN Systems, volume XXV, pages 981\u20131017, 1993.","journal-title":"Computer Networks and ISDN Systems"},{"issue":"5","key":"10_CR11","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"G. Holzmann. The SPIN model checker. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10_CR12","unstructured":"D. Jackson. Nitpick: A checkable specification language. In Proc. of the First ACM SIGSOFT Workshop on Formal Methods in Software Practice, pages 60\u201369, 1996."},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"D. Jackson, I. Schechter and I. Shlyakhter. Alcoa: the Alloy constraint analyser. In Int. Conf. on Software Engineering, 2000.","DOI":"10.1145\/337180.337616"},{"key":"10_CR14","unstructured":"J. Jacky and M. Patrick. Modelling, checking and implementing a control program for a radiation therapy machine. In R. Cleaveland, D. Jackson, editors, Proc. of the First ACM SIGPLAN Workshop on Automated Analysis of Software(AAS\u201997), pages 25\u201332, 1997."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"G. Kassel and G. Smith. Model checking Object-Z classes: Some experiments with FDR. In 8th Asia-Pacific Software Engineering Conference (APSEC 2001), IEEE Computer Society Press, 2001 (to appear).","DOI":"10.1109\/APSEC.2001.991513"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"F. Corella, Z. Zhou, X. Song, M. Langevin and E. Cerny. Multiway Decision Graphs for automated hardware verification. In Formal Methods in System Design, 10(1), 1997.","DOI":"10.1023\/A:1008663530211"},{"key":"10_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_44","volume-title":"11th Conference on Computer-Aided Verification (CAV\u201999)","author":"A. Cimatti","year":"1999","unstructured":"A. Cimatti, E.M. Clarke, F. Giunchiglia and M. Roveri. NuSMV: a new Symbolic Model Verifier. In N. Halbwachs and D. Peled, editors, 11th Conference on Computer-Aided Verification (CAV\u201999), vol. 1633 of LNCS, Springer-Verlag, 1999."},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"10_CR20","unstructured":"J.M. Spivey. The Z Notation-A Reference Manual. Prentice Hall, 1992."},{"issue":"5-6","key":"10_CR21","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/0950-5849(95)99365-T","volume":"37","author":"S. Valentine","year":"1995","unstructured":"S. Valentine. The programming language Z. Information and Software Technology, volume 37, number 5-6, pages 293\u2013301, May-June, 1995.","journal-title":"Information and Software Technology"},{"key":"10_CR22","series-title":"Lect Notes Comput Sci","volume-title":"8th Int. Conf. on Computer Aided Verifaction, (CAV\u201996)","author":"The VIS Group","year":"1996","unstructured":"The VIS Group. VIS: A System for Verification and Synthesis. In R. Alur and T. Henzinger, editors, 8th Int. Conf. on Computer Aided Verifaction, (CAV\u201996). vol. 1102 of LNCS, Springer-Verlag, 1996."},{"key":"10_CR23","volume-title":"PhD thesis","author":"K. Winter","year":"2001","unstructured":"K. Winter. Model Checking Abstract State Machines. PhD thesis, Technical University of Berlin, Germany, http:\/\/edocs.tu-berlin.de\/diss\/2001\/winter_kirsten.htm , 2001."},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"K. Winter. Model checking with abstract types. In S. Stoller and W. Visser, editors, Electronic Notes in Theoretical Computer Science, volume 55. Elsevier Science Publishers, 2001.","DOI":"10.1016\/S1571-0661(04)00264-6"},{"key":"10_CR25","unstructured":"P. Zave. Formal description of telecommunication services in Promela and Z. In Calculational System Design, Proc. of the Nineteenth International NATO Summer School. IOS Press, 1999."}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-47884-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T05:37:39Z","timestamp":1556429859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47884-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540437031","9783540478843"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-47884-1_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}