{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,2]],"date-time":"2026-02-02T13:35:24Z","timestamp":1770039324215,"version":"3.49.0"},"publisher-location":"Boston, MA","reference-count":13,"publisher":"Springer US","isbn-type":[{"value":"9780387754611","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-0-387-75462-8_14","type":"book-chapter","created":{"date-parts":[[2007,11,6]],"date-time":"2007-11-06T18:53:00Z","timestamp":1194375180000},"page":"189-204","source":"Crossref","is-referenced-by-count":18,"title":["Formal Modeling and Analysis of the Modbus Protocol"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Dutertre","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1_","doi-asserted-by":"crossref","unstructured":"P. Ammann, P. Black and W. Majurski, Using model checking to generate tests from specifications, Proceedings of the Second IEEE International Conference on Formal Engineering Methods, pp. 46-54, 1998.","DOI":"10.6028\/NIST.IR.6166"},{"key":"14_CR2_","first-page":"496","volume-title":"Proceedings of the Sixteenth International Conference on Computer Aided Verification (LNCS 3114)","author":"L de Moura","year":"2004","unstructured":"L. de Moura, S. Owre, H. Ruess, J. Rushby, N. Shankar, M. Sorea and A. Tiwari, SAL 2, in Proceedings of the Sixteenth International Conference on Computer Aided Verification (LNCS 3114), R. Alur and D. Peled (Eds. ), Springer, Berlin-Heidelberg, Germany, pp. 496-500, 2004."},{"key":"14_CR3_","volume-title":"The SAL Language Manual, Tech- nical Report SRI-CSL-01-02","author":"L de Moura","year":"2003","unstructured":"L. de Moura, S. Owre and N. Shankar, The SAL Language Manual, Tech- nical Report SRI-CSL-01-02, SRI International, Menlo Park, California, 2003."},{"key":"14_CR4_","volume-title":"Formal Modeling and Analysis of the Modbus Protocol","author":"B Dutertre","year":"2006","unstructured":"B. Dutertre, Formal Modeling and Analysis of the Modbus Protocol, Tech- nical Report, SRI International, Menlo Park, California, 2006."},{"key":"14_CR5_","first-page":"146","volume-title":"Proceedings of the Seventh Euro- pean Software Engineering Conference (LNCS 1687)","author":"A Gargantini","year":"1999","unstructured":"A. Gargantini and C. Heitmeyer, Using model checking to generate tests from requirements specifications, in Proceedings of the Seventh Euro- pean Software Engineering Conference (LNCS 1687), O. Nierstrasz and M. Lemoine (Eds. ), Springer, Berlin-Heidelberg, Germany, pp. 146-162, 1999."},{"key":"14_CR6_","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/BFb0031805","volume-title":"Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (LNCS 1166)","author":"D Geist","year":"1996","unstructured":"D. Geist, M. Farkas, A. Landver, Y. Lichtenstein, S. Ur and Y. Wolf- sthal, Coverage-directed test generation using symbolic techniques, in Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (LNCS 1166), M. Srivas and A. Camilleri (Eds. ), Springer, Berlin-Heidelberg, Germany, pp. 143-158, 1996."},{"key":"14_CR7_","doi-asserted-by":"crossref","unstructured":"G. Hamon, L. de Moura and J. Rushby, Generating efficient test sets with a model checker, Proceedings of the Second International Conference on Software Engineering and Formal Methods, pp. 261-270, 2004.","DOI":"10.1109\/SEFM.2004.1347530"},{"key":"14_CR8_","unstructured":"Modbus IDA, MODBUS Application Protocol Specification v1. 1a, North Grafton, Massachusetts ( www.modbus. org\/specs. php ), June 4, 2004."},{"key":"14_CR9_","unstructured":"Modbus IDA, MODBUS Messaging on TCP\/IP Implementation Guide v1. 0a, North Grafton, Massachusetts ( www.modbus. org\/specs. php ), June 4, 2004."},{"key":"14_CR10_","unstructured":"Modbus. org, MODBUS over Serial Line Specification and Implementation Guide v1. 0, North Grafton, Massachusetts ( www.modbus. org\/specs. php ), February 12, 2002."},{"issue":"2","key":"14_CR11_","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar and F. von Henke, Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS, IEEE Transactions on Software Engineering, vol. 21(2), pp. 107-125, 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"14_CR12_","doi-asserted-by":"crossref","unstructured":"S. Rayadurgam and M Heimdahl, Coverage based test-case generation using model checkers, Proceedings of the Eighth Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems, pp. 83-91, 2001.","DOI":"10.1109\/ECBS.2001.922409"},{"key":"14_CR13_","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-40911-4_20","volume-title":"Proceedings of the Second International Conference on Integrated Formal Methods (LNCS 1945)","author":"V Rusu","year":"2000","unstructured":"V. Rusu, L. du Bousquet and T. J\u00e9ron, An approach to symbolic test generation, in Proceedings of the Second International Conference on Integrated Formal Methods (LNCS 1945), W. Grieskamp, T. Santen and B. Stoddart (Eds. ), Springer, Berlin-Heidelberg, Germany, pp. 338-357, 2000."}],"container-title":["IFIP International Federation for Information Processing","Critical Infrastructure Protection"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-0-387-75462-8_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T12:46:39Z","timestamp":1684068399000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-0-387-75462-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9780387754611"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-75462-8_14","relation":{},"subject":[]}}