{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,15]],"date-time":"2025-07-15T03:25:04Z","timestamp":1752549904519},"publisher-location":"London","reference-count":10,"publisher":"Springer London","isbn-type":[{"type":"print","value":"9783540760702"},{"type":"electronic","value":"9781447109372"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/978-1-4471-0937-2_6","type":"book-chapter","created":{"date-parts":[[2011,10,10]],"date-time":"2011-10-10T15:23:02Z","timestamp":1318260182000},"page":"73-82","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification as a Design Tool - The Transponder Lock Example"],"prefix":"10.1007","author":[{"given":"R.","family":"Budde","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Merceron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K.-H.","family":"Sylla","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"A. Benveniste and G. Berry. The synchronous approach to reactive and real-time systems. Proceedings of the IEEE, 79(9), 1991.","DOI":"10.1109\/5.97297"},{"key":"6_CR2","volume-title":"Object-Oriented Software Engineering A Use Case Driven Approach","author":"I Jacobson","year":"1992","unstructured":"Ivar Jacobson, Magnus Christerson, Parik Jonsson, and Gunnar \u00d6vergard. Object-Oriented Software Engineering A Use Case Driven Approach. Addison-Wesley, 1992."},{"key":"6_CR3","series-title":"SIGPLAN Notices","first-page":"1","volume-title":"A laboratory for teaching object-oriented thinking","author":"K Beck","year":"1989","unstructured":"Kent Beck and Ward Cunningham. A laboratory for teaching object-oriented thinking. Number 24(10) in SIGPLAN Notices, pages 1\u20136. SIGPLAN, October 1989."},{"key":"6_CR4","volume-title":"Boolean automata for implementing ESTEREL","author":"A Poign\u00e9","year":"1995","unstructured":"A. Poign\u00e9 and L. Holenderski. Boolean automata for implementing ESTEREL. Arbeitspapiere der GMD 964, Forschungszentrum Informationstechnik GmbH, December 1995."},{"issue":"1","key":"6_CR5","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. Halpern. \u2018sometimes\u2019 and \u2018not never\u2019 revisited: On branching versus linear time temporal logic. Journal Of the Association for Computing Machinery, 33(1):151\u2013178, 1986.","journal-title":"Journal Of the Association for Computing Machinery"},{"key":"6_CR6","volume-title":"Arbeitspapiere der GMD 972, Forschungszentrum Informationstechnik GmbH","author":"A Merceron","year":"1996","unstructured":"A. Merceron. Checking synchronous programs using automatic abstraction, modular verification and assumption discharge. Arbeitspapiere der GMD 972, Forschungszentrum Informationstechnik GmbH, January 1996."},{"key":"6_CR7","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"L McMillan","year":"1992","unstructured":"K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon, 1992."},{"key":"6_CR8","unstructured":"Vis user\u2019s manual. The VIS Group, December 1995. available in \n                  http:\/\/www-cad. eecs.berkeley.edu\/Respep\/Research\/vis\/doc"},{"key":"6_CR9","series-title":"Lecture Notes in Artificial Intelligence","first-page":"748","volume-title":"PVS: A prototype verification system","author":"S Owre","year":"1992","unstructured":"S. Owre, J.M. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 748\u2013752. Springer-Verlag, 1992."},{"key":"6_CR10","first-page":"54","volume-title":"OBJEKT-spektrum","author":"R Budde","year":"1995","unstructured":"R. Budde and K.-H. Sylla. Objektorientierte Echtzeit-Anwendungen auf Grundlage perfekter Synchronisation und: Eingebettete Echtzeitsysteme. OBJEKT-spektrum, (2 and 4):54\u201360 and 10\u201316, 1995."}],"container-title":["Safe Comp 96"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4471-0937-2_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,1]],"date-time":"2021-05-01T00:57:37Z","timestamp":1619830657000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4471-0937-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540760702","9781447109372"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-1-4471-0937-2_6","relation":{},"subject":[],"published":{"date-parts":[[1997]]}}}