{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:24:56Z","timestamp":1762521896151},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319336923"},{"type":"electronic","value":"9783319336930"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-33693-0_32","type":"book-chapter","created":{"date-parts":[[2016,5,24]],"date-time":"2016-05-24T05:35:47Z","timestamp":1464068147000},"page":"508-522","source":"Crossref","is-referenced-by-count":39,"title":["Formal Verification of Safety PLC Based Control Software"],"prefix":"10.1007","author":[{"given":"D\u00e1niel","family":"Darvas","sequence":"first","affiliation":[]},{"given":"Istv\u00e1n","family":"Majzik","sequence":"additional","affiliation":[]},{"given":"Enrique","family":"Blanco Vi\u00f1uela","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,5,24]]},"reference":[{"key":"32_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1007\/978-3-319-25423-4_15","volume-title":"Formal Methods and Software Engineering","author":"B Beckert","year":"2015","unstructured":"Beckert, B., Ulbrich, M., Vogel-Heuser, B., Weigl, A.: Regression verification for programmable logic controller software. In: Butler, M., Conchon, M., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 234\u2013251. Springer, Heidelberg (2015)"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Biallas, S., Brauer, J., Kowalewski, S.: Arcade.PLC: a verification platform for programmable logic controllers. In: Proceedings of 27th IEEE\/ACM International Conference on Automated Software Engineering, pp. 338\u2013341. ACM (2012)","DOI":"10.1145\/2351676.2351741"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Canet, G., Couffin, S., Lesage, J.J., Petit, A., Schnoebelen, P.: Towards the automatic verification of PLC programs written in instruction list. In: Proceedings of IEEE International Conference on Systems, Man, and Cybernetics, vol. 4, pp. 2449\u20132454. IEEE (2000)","DOI":"10.1109\/ICSMC.2000.884359"},{"key":"32_CR4","unstructured":"Darvas, D., Blanco Vi\u00f1uela, E., Majzik, I.: A formal specification method for PLC-based applications. In: Proceedings of 15th International Conference on Accelerator & Large Experimental Physics Control Systems, pp. 907\u2013910. JaCoW, Geneva (2015, in press)"},{"key":"32_CR5","unstructured":"Darvas, D., Fern\u00e1ndez Adiego, B., Blanco Vi\u00f1uela, E.: PLCverif: a tool to verify PLC programs based on model checking techniques. In: Proceedings of 15th International Conference on Accelerator & Large Experimental Physics Control Systems, pp. 911\u2013914. JaCoW, Geneva (2015, in press)"},{"key":"32_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/978-3-662-43613-4_18","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"D Darvas","year":"2014","unstructured":"Darvas, D., Fern\u00e1ndez Adiego, B., V\u00f6r\u00f6s, A., Bartha, T., Blanco Vi\u00f1uela, E., Gonz\u00e1lez Su\u00e1rez, V.M.: Formal verification of complex properties on PLC programs. In: \u00c1brah\u00e1m, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 284\u2013299. Springer, Heidelberg (2014)"},{"issue":"6","key":"32_CR7","doi-asserted-by":"crossref","first-page":"1400","DOI":"10.1109\/TII.2015.2489184","volume":"11","author":"B Fern\u00e1ndez Adiego","year":"2015","unstructured":"Fern\u00e1ndez Adiego, B., Darvas, D., Blanco Vi\u00f1uela, E., Tournier, J.C., Bliudze, S., Blech, J.O., Gonz\u00e1lez Su\u00e1rez, V.M.: Applying model checking to industrial-sized PLC programs. IEEE. Trans. Ind. Informat. 11(6), 1400\u20131410 (2015)","journal-title":"IEEE. Trans. Ind. Informat."},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"Gourcuff, V., de Smet, O., Faure, J.M.: Improving large-sized PLC programs verification using abstractions. In: Proceedings of the 17th IFAC World Congress, pp. 5101\u20135106. IFAC (2008)","DOI":"10.3182\/20080706-5-KR-1001.00857"},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"Greenway, A.: A user\u2019s perspective of programmable logic controllers (PLCs) in safety-related applications. In: Redmill, F., Anderson, T. (eds.) Technology and Assessment of Safety-Critical Systems, pp. 1\u201320. Springer, London (1994)","DOI":"10.1007\/978-1-4471-2082-7_1"},{"issue":"3","key":"32_CR10","first-page":"171","volume":"42","author":"E Jee","year":"2010","unstructured":"Jee, E., et al.: FBDVerifier: interactive and visual analysis of counterexample in formal verification of function block diagram. J. Res. Pract. Inf. Technol. 42(3), 171\u2013188 (2010)","journal-title":"J. Res. Pract. Inf. Technol."},{"key":"32_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1007\/978-3-319-03077-7_4","volume-title":"Hardware and Software: Verification and Testing","author":"T Lange","year":"2013","unstructured":"Lange, T., Neuh\u00e4u\u00dfer, M.R., Noll, T.: Speeding up the safety verification of programmable logic controller code. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 44\u201360. Springer, Heidelberg (2013)"},{"key":"32_CR12","series-title":"Advances in Intelligent Systems and Computing","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-3-319-16577-6_3","volume-title":"Formalisms for Reuse and Systems Integration","author":"J Nellen","year":"2015","unstructured":"Nellen, J., \u00c1brah\u00e1m, E., Wolters, B.: A CEGAR tool for the reachability analysis of PLC-controlled plants using hybrid automata. In: Bouabana-Tebibel, T., Rubin, S.H. (eds.) Formalisms for Reuse and Systems Integration. AISC, vol. 346, pp. 55\u201378. Springer, Heidelberg (2015)"},{"key":"32_CR13","doi-asserted-by":"crossref","unstructured":"Ovatman, T., Aral, A., Polat, D., \u00dcnver, A.O.: An overview of model checking practices on verification of PLC software. Software & Systems Modeling, 1\u201324 (2014). doi: 10.1007\/s10270-014-0448-7 . Advance online publication","DOI":"10.1007\/s10270-014-0448-7"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Pavlovi\u0107, O., Ehrich, H.D.: Model checking PLC software written in function block diagram. In: Proceedings of International Conference on Software Testing, Verification and Validation, pp. 439\u2013448. IEEE (2010)","DOI":"10.1109\/ICST.2010.10"},{"key":"32_CR15","doi-asserted-by":"crossref","unstructured":"Sarmento, C.A., Silva, J.R., Miyagi, P.E., Santos Filho, D.J.: Modeling of programs and its verification for programmable logic controllers. In: Proceedings of the 17th IFAC World Congress, pp. 10546\u201310551. IFAC (2008)","DOI":"10.3182\/20080706-5-KR-1001.01786"},{"key":"32_CR16","unstructured":"Siemens: Statement List (STL) for S7\u2013300\/S7-400, C79000\u2013G7076-C565-01 (1998)"},{"key":"32_CR17","unstructured":"Siemens: SIMATIC Industrial Software SIMATIC safety \u2013 Configuring and Programming, A5E02714440-AD (2014)"},{"issue":"9","key":"32_CR18","doi-asserted-by":"crossref","first-page":"929","DOI":"10.1016\/j.conengprac.2011.01.001","volume":"19","author":"D Soliman","year":"2011","unstructured":"Soliman, D., Frey, G.: Verification and validation of safety applications based on PLCopen safety function blocks. Control Eng. Pract. 19(9), 929\u2013946 (2011)","journal-title":"Control Eng. Pract."},{"key":"32_CR19","unstructured":"S\u00fclflow, A., Drechsler, R.: Verification of PLC programs using formal proof techniques. In: Formal Methods for Automation and Safety in Railway and Automotive Systems, pp. 43\u201350. L\u2019Harmattan, Budapest (2008)"},{"key":"32_CR20","doi-asserted-by":"crossref","unstructured":"Yoo, J., Cha, S., Jee, E.: A verification framework for FBD based software in nuclear power plants. In: Proceedings of the 15th Asia-Pacific Software Engineering Conference, pp. 385\u2013392. IEEE (2008)","DOI":"10.1109\/APSEC.2008.26"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33693-0_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T14:43:53Z","timestamp":1498315433000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33693-0_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319336923","9783319336930"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33693-0_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}