{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T12:39:39Z","timestamp":1756384779849},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642169007"},{"type":"electronic","value":"9783642169014"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16901-4_20","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T17:40:06Z","timestamp":1289238006000},"page":"287-302","source":"Crossref","is-referenced-by-count":2,"title":["A Formal Verification Study on the Rotterdam Storm Surge Barrier"],"prefix":"10.1007","author":[{"given":"Ken","family":"Madlener","sequence":"first","affiliation":[]},{"given":"Sjaak","family":"Smetsers","sequence":"additional","affiliation":[]},{"given":"Marko","family":"van Eekelen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"5","key":"20_CR1","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"6","key":"20_CR2","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1109\/MC.2006.212","volume":"39","author":"G.J. Holzmann","year":"2006","unstructured":"Holzmann, G.J.: The power of 10: Rules for developing safety-critical code. IEEE Computer\u00a039(6), 95\u201397 (2006)","journal-title":"IEEE Computer"},{"key":"20_CR3","unstructured":"IEC: Functional safety: Safety related systems, International Standard IEC 61508, International Electrotechnical Commission, Geneva, Switzerland (1996)"},{"key":"20_CR4","unstructured":"Jia, X.: ZTC: A Type Checker for Z \u2013 User\u2019s Guide. Institute for Software Engineering, Department of Computer Science and Information Systems, DePaul University, Chicago, USA (1994)"},{"key":"20_CR5","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","volume-title":"Proc. of SPIN 1996: The Second Workshop on the SPIN Verification System","author":"P. Kars","year":"1996","unstructured":"Kars, P.: The application of Promela and SPIN in the BOS project. In: Gr\u00e9goire, J.-C., Holzmann, G.J., Peled, D.A. (eds.) Proc. of SPIN 1996: The Second Workshop on the SPIN Verification System. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a032. Rutgers University, New Jersey, USA (1996)"},{"key":"20_CR6","unstructured":"Kars, P.: Formal methods in the design of a storm surge barrier control system. In: Lectures on Embedded Systems, European Educational Forum, School on Embedded Systems (1996)"},{"issue":"7","key":"20_CR7","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"key":"20_CR8","unstructured":"Owre, S.: Random testing in PVS. In: Workshop on Automated Formal Methods, Seattle, USA (2006), \n                    \n                      http:\/\/fm.csl.sri.com\/AFM06\/papers\/5-Owre.pdf"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"20_CR10","unstructured":"Ruys, T.: Towards Effective Model Checking. PhD thesis, University of Twente (2001)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/BFb0027284","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"M. Saaltink","year":"1997","unstructured":"Saaltink, M.: The Z\/Eves system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol.\u00a01212, pp. 72\u201388. Springer, Heidelberg (1997)"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/978-3-642-04570-7_12","volume-title":"FMICS 2009","author":"E. Schierboom","year":"2009","unstructured":"Schierboom, E., Tamalet, A., Tews, H., van Eekelen, M., Smetsers, S.: Preemption abstraction: A lightweight approach to modelling concurrency. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol.\u00a05825, pp. 149\u2013164. Springer, Heidelberg (2009)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-48257-1_25","volume-title":"Applied Formal Methods - FM-Trends 98","author":"O. Slotosch","year":"1999","unstructured":"Slotosch, O.: Overview over the project Quest. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol.\u00a01641, pp. 346\u2013350. Springer, Heidelberg (1999)"},{"key":"20_CR14","unstructured":"Spivey, J.M.: The Z notation: a reference manual. Prentice-Hall International Series in Computer Science (1989)"},{"issue":"2","key":"20_CR15","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1023\/A:1011236117591","volume":"19","author":"J. Tretmans","year":"2001","unstructured":"Tretmans, J., Wijbrans, K., Chaudron, M.: Software engineering with formal methods: The development of a storm surge barrier control system revisiting seven myths of formal methods. Formal Methods in System Design\u00a019(2), 195\u2013215 (2001)","journal-title":"Formal Methods in System Design"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-540-68237-0_30","volume-title":"FM 2008: Formal Methods","author":"K. Wijbrans","year":"2008","unstructured":"Wijbrans, K., Buve, F., Rijkers, R., Geurts, W.: Software engineering with formal methods: Experiences with the development of a storm surge barrier control system. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 419\u2013424. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16901-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T04:03:48Z","timestamp":1553227428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}