{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T20:58:15Z","timestamp":1648760295728},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T00:00:00Z","timestamp":1194566400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Informatik Forsch. Entw."],"published-print":{"date-parts":[[2008,2]]},"DOI":"10.1007\/s00450-007-0032-2","type":"journal-article","created":{"date-parts":[[2007,11,8]],"date-time":"2007-11-08T04:34:07Z","timestamp":1194496447000},"page":"95-108","source":"Crossref","is-referenced-by-count":2,"title":["An industrial application of symbolic model checking"],"prefix":"10.1007","volume":"22","author":[{"given":"Florian","family":"Kamm\u00fcller","sequence":"first","affiliation":[]},{"given":"S\u00f6ren","family":"Preibusch","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,11,9]]},"reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"B\u00e4umler S, Balser M, Dunets A, Reif W, Schmitt J (2006) Verification of Medical Guidelines by Model Checking \u2013 A Case Study http:\/\/spinroot.com\/spin\/Workshops\/ws06\/027.pdf","DOI":"10.1007\/11691617_13"},{"key":"32_CR2","unstructured":"Bundesamt f\u00fcr Sicherheit in der Informationsgesellschaft (BSI) (2005) Common Criteria for Information Technology Security Evaluation, Part 3. http:\/\/www.bsi.de\/cc\/ccpart3v2_3.pdf"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Burch JR, Clarke EM, Long DE (1994) Symbolic Model Checking for Sequential Circuit Verification. IEEE Trans Comp Aided Design Integr Circ Syst 13:401\u2013424","DOI":"10.1109\/43.275352"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Chan W, Anderson RJ, Beame P, Burns S, Modugno F, Notkin D, Reese JD (1998) Model checking large software specifications. IEEE Trans Softw Eng 24(7):498\u2013520","DOI":"10.1109\/32.708566"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke EM, Giunchiglia F, Roveri M (2000) NuSMV: a new symbolic model verifier. In: Halbwachs N, Peled D (eds) International Conference on Computer-Aided Verification (CAV\u201999), LNCS, vol 1633, pp 495\u2013499, Springer, Berlin Heidelberg","DOI":"10.1007\/3-540-48683-6_44"},{"key":"32_CR6","unstructured":"Cimatti A (2000). Industrial Applications of Model Checking. In: Cassez F, Jard C, Rozoy B, Ryan MD (eds.) Modeling and Verification of Parallel Processes (MOVEP\u201900), LNCS, vol. 2067, pp 153\u2013167, Springer, Berlin Heidelberg"},{"key":"32_CR7","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model Checking. The MIT Press, Cambridge, MA, USA"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"Helke S, Kamm\u00fcller F (2005) Property Preserving Abstraction for Statecharts. In: 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2005, LNCS, vol. 3731, pp 305\u2013319, Springer, Berlin Heidelberg","DOI":"10.1007\/11562436_23"},{"key":"32_CR9","volume-title":"Design and Verification of Computer Protocols","author":"GJ Holzmann","year":"1991","unstructured":"Holzmann GJ (1991) Design and Verification of Computer Protocols. Prentice Hall, London"},{"key":"32_CR10","doi-asserted-by":"crossref","unstructured":"Janssen W, Mateescu R, Mauw S, Fennema P, van der Stappen P (1999) Model checking for managers. In: Proceedings Theoretical and Practical Aspects of SPIN Model Checking, LNCS, vol 1680, pp 92\u2013107, Springer, Berlin Heidelberg","DOI":"10.1007\/3-540-48234-2_7"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"Lamport L (1994) The temporal logic of actions. ACM Trans Prog Lang Syst 16:872\u2013923 http:\/\/doi.acm.org\/10.1145\/177492.177726","DOI":"10.1145\/177492.177726"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Larsen K G, Steffen B, Weise C (1997) Continuous Modelling of Real Time and Hybrid Systems: From Concepts to Tools. Int J Softw Tools Technol Transf 1:64\u201385","DOI":"10.1007\/s100090050006"},{"key":"32_CR13","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z Manna","year":"1991","unstructured":"Manna Z, Pnueli A (1991) The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York"},{"key":"32_CR14","unstructured":"McMillan KL (1992) Symbolic Model Checking \u2013 an Approach to the State Explosion Problem. School of Computer Science, Pittsburgh PA, Carnegie Mellon University"},{"key":"32_CR15","volume-title":"Symbolic Model Checking","author":"KL McMillan","year":"1995","unstructured":"McMillan KL (1995) Symbolic Model Checking. Kluwer Academic Publishers, Norwell, MA, USA"},{"key":"32_CR16","unstructured":"nuSMV (1999) NuSMV examples: the collection. http:\/\/nusmv.irst.itc.it\/examples\/examples.html"},{"key":"32_CR17","unstructured":"Preibusch S (2006) http:\/\/preibusch.de\/projects\/TWIN\/"},{"key":"32_CR18","unstructured":"ThyssenKrupp (2005) Safe distance \u2013 Four-level safety concept. http:\/\/twin-elevator.com\/Safe_distance.353.0.html?L=1"},{"key":"32_CR19","unstructured":"ThyssenKrupp (2005) Higher performance. http:\/\/twin-elevator.com\/New_buildings.368.0.html?L=1"},{"key":"32_CR20","unstructured":"Uppsala University, Department of Information Technology (2006) UPPAAL. http:\/\/www.uppaal.com\/"}],"container-title":["Informatik - Forschung und Entwicklung"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00450-007-0032-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00450-007-0032-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00450-007-0032-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T09:32:44Z","timestamp":1559122364000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00450-007-0032-2"}},"subtitle":["The TWIN elevator case study"],"short-title":[],"issued":{"date-parts":[[2007,11,9]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,2]]}},"alternative-id":["32"],"URL":"https:\/\/doi.org\/10.1007\/s00450-007-0032-2","relation":{},"ISSN":["0178-3564","0949-2925"],"issn-type":[{"value":"0178-3564","type":"print"},{"value":"0949-2925","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,11,9]]}}}