{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,24]],"date-time":"2026-06-24T15:43:01Z","timestamp":1782315781084,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662436127","type":"print"},{"value":"9783662436134","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-43613-4_18","type":"book-chapter","created":{"date-parts":[[2014,5,20]],"date-time":"2014-05-20T03:56:40Z","timestamp":1400558200000},"page":"284-299","source":"Crossref","is-referenced-by-count":26,"title":["Formal Verification of Complex Properties on PLC Programs"],"prefix":"10.1007","author":[{"given":"D\u00e1niel","family":"Darvas","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Borja","family":"Fern\u00e1ndez Adiego","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tam\u00e1s","family":"Bartha","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Enrique","family":"Blanco Vi\u00f1uela","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"V\u00edctor M.","family":"Gonz\u00e1lez Su\u00e1rez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Darvas, D., Fern\u00e1ndez, B., Blanco, E.: Transforming PLC programs into formal models for verification purposes. Internal note, CERN (2013), http:\/\/cds.cern.ch\/record\/1629275\/files\/CERN-ACC-NOTE-2013-0040.pdf"},{"key":"18_CR2","unstructured":"IEC 61131: Programming languages for programmable logic controllers (2013)"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Rausch, M., Krogh, B.: Formal verification of PLC programs. In: Proc. of the American Control Conference, pp. 234\u2013238 (1998)","DOI":"10.1109\/ACC.1998.694666"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-540-27863-4_28","volume-title":"Integration of Software Specification Techniques for Applications in Engineering","author":"N. Bauer","year":"2004","unstructured":"Bauer, N., Engell, S., Huuck, R., Lohmann, S., Lukoschus, B., Remelhe, M., Stursberg, O.: Verification of PLC programs given as sequential function charts. In: Ehrig, H., Damm, W., Desel, J., Gro\u00dfe-Rhode, M., Reif, W., Schnieder, E., Westk\u00e4mper, E. (eds.) INT 2004. LNCS, vol.\u00a03147, pp. 517\u2013540. Springer, Heidelberg (2004)"},{"key":"18_CR5","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: Proc. of Int. Conf. on Systems, Man, and Cybernetics 2000, pp. 2449\u20132454. Argos Press (2000)","DOI":"10.1109\/ICSMC.2000.884359"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Pavlovi\u0107, O., Ehrich, H.D.: Model checking PLC software written in function block diagram. In: International Conference on Software Testing, pp. 439\u2013448 (2010)","DOI":"10.1109\/ICST.2010.10"},{"issue":"9","key":"18_CR7","doi-asserted-by":"publisher","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 Engineering Practice\u00a019(9), 929\u2013946 (2011)","journal-title":"Control Engineering Practice"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Gourcuff, V., de Smet, O., Faure, J.M.: Improving large-sized PLC programs verification using abstractions. In: 17th IFAC World Congress (2008)","DOI":"10.3182\/20080706-5-KR-1001.00857"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Noll, T.: Speeding up the safety verification of programmable logic controller code. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol.\u00a08244, pp. 44\u201360. Springer, Heidelberg (2013)"},{"key":"18_CR10","unstructured":"Biallas, S., Brauer, J., Kowalewski, S.: Counterexample-guided abstraction refinement for PLCs. In: Proc. of 5th International Workshop on Systems Software Verification, pp. 2\u201312. USENIX Association (2010)"},{"key":"18_CR11","unstructured":"Blanco, E., et al.: UNICOS evolution: CPC version 6. In: 12th ICALEPCS (2011)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol.\u00a03185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"key":"18_CR13","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (1999)"},{"key":"18_CR14","unstructured":"Cavada, R., Cimatti, A., Jochim, C.A., Keighren, G., Olivetti, E., Pistore, M., Roveri, M., Tchaltsev, A.: NuSMV 2.5 User Manual. FBK-irst (2011)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"18_CR16","unstructured":"Cooper, K.D., Torczon, L.: Engineering a Compiler, 2nd edn. Morgan Kaufmann Publishers Inc. (2012)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-43613-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,10]],"date-time":"2019-08-10T12:40:26Z","timestamp":1565440826000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-43613-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662436127","9783662436134"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-43613-4_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}