{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,30]],"date-time":"2025-01-30T06:22:09Z","timestamp":1738218129340,"version":"3.34.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797067"},{"type":"electronic","value":"9783540797074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79707-4_5","type":"book-chapter","created":{"date-parts":[[2008,5,7]],"date-time":"2008-05-07T06:37:44Z","timestamp":1210142264000},"page":"38-55","source":"Crossref","is-referenced-by-count":3,"title":["Checking the TWIN Elevator System by Translating Object-Z to SMV"],"prefix":"10.1007","author":[{"given":"S\u00f6ren","family":"Preibusch","sequence":"first","affiliation":[]},{"given":"Florian","family":"Kamm\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Amnell, T.: Code Synthesis for Timed Automata. Thesis, Uppsala University (2003)"},{"key":"5_CR2","unstructured":"The Community Z Tools project (2006), http:\/\/czt.sourceforge.net\/"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Algebraic Methodology and Software Technology","author":"J. Derrick","year":"2004","unstructured":"Derrick, J., Smith, G.: Linear temporal logic and Z refinement. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116. Springer, Heidelberg (2004)"},{"key":"5_CR4","unstructured":"Duke, R., Rose, G.: Formal Object-Oriented Specification Using Object-Z. Cornerstones of Computing. MacMillan (2000)"},{"key":"5_CR5","unstructured":"International Organization for Standardization: ISO\/IEC 13568:2002: Information technology \u2013 Z formal specification notation \u2013 Syntax, type system and semantics, http:\/\/www.iso.ch\/iso\/en\/CatalogueDetailPage.CatalogueDetail?CSNUMBER=21573"},{"key":"5_CR6","unstructured":"Kamm\u00fcller, F.: Interactive Theorem Proving in Software Engineering. In: Habilitationsschrift, Technische Universit\u00e4t Berlin (2006)"},{"key":"5_CR7","volume-title":"Informatik Forschung und Entwicklung","author":"F. Kamm\u00fcller","year":"2007","unstructured":"Kamm\u00fcller, F., Preibusch, S.: An Industrial Application of Symbolic Model Checking \u2013 The TWIN-Elevator Case Study. In: Informatik Forschung und Entwicklung. Springer, Heidelberg (accepted for publication, 2007)"},{"key":"5_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07287-5","volume-title":"Formal Engineering for Industrial Software Development","author":"S. Liu","year":"2004","unstructured":"Liu, S.: Formal Engineering for Industrial Software Development. Springer, Heidelberg (2004)"},{"key":"5_CR9","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1995","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1995)"},{"key":"5_CR10","unstructured":"Preibusch, S.: TWIN Elevator System, Concise Object-Z Specification (2007) http:\/\/preibusch.de\/projects\/TWIN\/Concise_OZ"},{"key":"5_CR11","unstructured":"Preibusch, S.: TWIN Elevator System, Concise Object-Z Specification (Translation to SMV) (2007), http:\/\/preibusch.de\/projects\/TWIN\/Concise_OZ_Translation_SMV"},{"key":"5_CR12","volume-title":"Advances in Formal Methods","author":"G. Smith","year":"2000","unstructured":"Smith, G.: The Object-Z Specification Language. In: Advances in Formal Methods. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45648-1_5","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"G. Smith","year":"2002","unstructured":"Smith, G., Kamm\u00fcller, F., Santen, T.: Encoding Object-Z in Isabelle\/HOL. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272. Springer, Heidelberg (2002)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b105497","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"G. Smith","year":"2005","unstructured":"Smith, G., Wildman, L.: Model Checking Z Specifications Using SAL. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol.\u00a03455. Springer, Heidelberg (2005)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44880-2_17","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"G. Smith","year":"2003","unstructured":"Smith, G., Winter, K.: Proving temporal properties of Z specifications using abstraction. In: Bert, D., P. Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol.\u00a02651. Springer, Heidelberg (2003)"},{"key":"5_CR16","unstructured":"Software Design Group, MIT Computer Science and Artificial Intelligence Laboratory. The Alloy Analyzer (2007), http:\/\/alloy.mit.edu\/"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"ThyssenKrupp Elevator. TWIN Report (2005), http:\/\/www.twin.thyssenkrupp-elevator.de\/?&L=1","DOI":"10.1049\/ic:20050208"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Integrated Formal Methods","author":"K. Winter","year":"2002","unstructured":"Winter, K., Duke, R.: Model Checking Object-Z using ASM. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol.\u00a02335. Springer, Heidelberg (2002)"},{"key":"5_CR19","unstructured":"The World Wide Web Virtual Library: The Z notation. Tool support (2005), http:\/\/vl.zuser.org\/#tools"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79707-4_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,30]],"date-time":"2025-01-30T03:52:09Z","timestamp":1738209129000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79707-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797067","9783540797074"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79707-4_5","relation":{},"subject":[]}}