{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T17:36:28Z","timestamp":1777656988056,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642308840","type":"print"},{"value":"9783642308857","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30885-7_30","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T04:50:45Z","timestamp":1340772645000},"page":"353-356","source":"Crossref","is-referenced-by-count":10,"title":["Formal Verification of PLC Programs Using the B Method"],"prefix":"10.1007","author":[{"given":"Haniel","family":"Barbosa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"D\u00e9harbe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","unstructured":"IEC: IEC 61131-3 - Programmable controllers. International Electrotechnical Comission Standards (2003)"},{"key":"30_CR2","unstructured":"Abrial, Jr.: The B-book: assigning programs to meanings. Cambridge University Press, Cambridge (2005)"},{"key":"30_CR3","unstructured":"PLCopen: XML Formats for IEC 61131-3. PLCopen Technical Committee 6 (2009)"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Farines, J., de Queiroz, M.H., da Rocha, V.G., Carpes, A.A.M., Vernadat, F., Cr\u00e9gut, X.: A model-driven engineering approach to formal verification of PLC programs. In: IEEE EFTA (2011)","DOI":"10.1109\/ETFA.2011.6058983"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Ljungkrantz, O., \u00c5kesson, K., Fabian, M., Yuan, C.: A Formal Specification language for PLC-based Control Logic. In: Proc. of 8th IEEE International Conference on Industrial Informatics, pp. 1067\u20131072 (2010)","DOI":"10.1109\/INDIN.2010.5549591"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Soliman, D., Frey, G.: Verification and Validation of Safety Applications based on PLcopen Safety Function Blocks using Timed Automata in Uppaal. In: Proceedings of the Second IDAC Workshop on Dependable Control of Discrete Systems (DCDS), pp. 39\u201344 (2009)","DOI":"10.3182\/20090610-3-IT-4004.00011"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30885-7_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:33:15Z","timestamp":1620113595000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30885-7_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642308840","9783642308857"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30885-7_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}