{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T00:31:41Z","timestamp":1787013101591,"version":"build-2736575974"},"reference-count":39,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"6","license":[{"start":{"date-parts":[[2015,12,1]],"date-time":"2015-12-01T00:00:00Z","timestamp":1448928000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Ind. Inf."],"published-print":{"date-parts":[[2015,12]]},"DOI":"10.1109\/tii.2015.2489184","type":"journal-article","created":{"date-parts":[[2015,10,9]],"date-time":"2015-10-09T14:53:48Z","timestamp":1444402428000},"page":"1400-1410","source":"Crossref","is-referenced-by-count":67,"title":["Applying Model Checking to Industrial-Sized PLC Programs"],"prefix":"10.1109","volume":"11","author":[{"given":"Borja","family":"Fernandez Adiego","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Darvas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Enrique Blanco","family":"Vinuela","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Charles","family":"Tournier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Simon","family":"Bliudze","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan Olaf","family":"Blech","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Victor Manuel","family":"Gonzalez Suarez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/978-3-642-24690-6_6","article-title":"Verification of PLC properties based on formal semantics in Coq","author":"blech","year":"2011","journal-title":"Software Engineering and Formal Methods"},{"key":"ref38","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/3-540-46002-0_21","article-title":"The ForSpec temporal logic: A new temporal property-specification language","author":"armoni","year":"2002","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref33","first-page":"394","article-title":"Bringing automated model checking to PLC program development—A CERN case study","author":"fern\u00e1ndez adiego","year":"0","journal-title":"Proc Int Workshop Discrete Event Syst"},{"key":"ref32","first-page":"334","article-title":"The nuXmv symbolic model checker","author":"cavada","year":"2014","journal-title":"Computer Aided Verification"},{"key":"ref31","year":"2011","journal-title":"Standards Compliance According to IEC 61131-3"},{"key":"ref30","first-page":"a5e02789666","year":"2010","journal-title":"SIMATIC Programming With STEP7—Manual"},{"key":"ref37","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","article-title":"The temporal logic Sugar","author":"beer","year":"2001","journal-title":"Computer Aided Verification"},{"key":"ref36","first-page":"411","article-title":"Patterns in property specifications for finite-state verification","author":"dwyer","year":"0","journal-title":"Proc 21st Int Conf Softw Eng"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"ref34","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/s10009-003-0132-7","article-title":"Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) infusion pump control system","volume":"5","author":"alur","year":"2004","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2012.05.002"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2010.2050199"},{"key":"ref12","first-page":"10 546","article-title":"Modeling of programs and its verification for programmable logic controllers","author":"sarmento","year":"0","journal-title":"Proc 17th Int Fed Autom Control World Congr"},{"key":"ref13","first-page":"439","article-title":"Model checking PLC software written in function block diagram","author":"pavlovi?","year":"0","journal-title":"Proc of Int'l Conf on Softw Testing Verif and Valid"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2011.01.001"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2000.884359"},{"key":"ref16","first-page":"472","article-title":"Verification of an industrial safety function using coloured Petri nets and model checking","author":"bartha","year":"0","journal-title":"Proc 14th Int Conf Mod Inf Technol Innov Processes Ind Entrep (MITIP)"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1007\/978-3-540-27863-4_28","article-title":"Verification of PLC programs given as sequential function charts","author":"bauer","year":"2004","journal-title":"Integration of Software Specification Techniques for Applications in Engineering"},{"key":"ref18","first-page":"10","article-title":"Counterexample-guided abstraction refinement for PLCs","author":"biallas","year":"0","journal-title":"Proc 5th Int Conf Syst Softw"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2008.26"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24732-6_22"},{"key":"ref4","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/978-3-662-43613-4_18","article-title":"Formal verification of complex properties on PLC programs","author":"darvas","year":"2014","journal-title":"Formal Techniques for Distributed Objects Components and Systems"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1002\/9780470611012.ch10"},{"key":"ref3","article-title":"Automated generation of formal models from ST control programs for verification purposes","author":"fern\u00e1ndez adiego","year":"2014"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2000.884356"},{"key":"ref29","year":"2013"},{"key":"ref5","first-page":"3333","article-title":"Modelling and formal verification of timing aspects in large PLC programs","author":"fern\u00e1ndez adiego","year":"0","journal-title":"Proc World Congr Int Fed Autom Control"},{"key":"ref8","first-page":"43","article-title":"Verification of PLC programs using formal proof techniques","author":"s\u00fclflow","year":"2008","journal-title":"Formal Methods for Automation and Safety in Railway and Automotive Systems"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/EMRTS.1999.777456"},{"key":"ref2","first-page":"722","article-title":"Model-based automated testing of critical PLC programs","author":"fern\u00e1ndez adiego","year":"0","journal-title":"Proc IEEE Int Conf Ind Informatics"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.arcontrol.2012.09.015"},{"key":"ref1","year":"2010"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24704-5_15"},{"key":"ref22","first-page":"5101","article-title":"Improving large-sized PLC programs verification using abstractions","author":"gourcuff","year":"0","journal-title":"Proc 17th Int Fed Autom Control World Congr"},{"key":"ref21","first-page":"65","article-title":"Conversion of ST control programs to ANSI C for verification purposes","volume":"5","author":"sadolewski","year":"2011","journal-title":"Informatica Exame"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-16577-6_3"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03077-7_4"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-014-0448-7"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.3103\/S0146411614070244"}],"container-title":["IEEE Transactions on Industrial Informatics"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9424\/7343788\/07295624.pdf?arnumber=7295624","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T11:46:09Z","timestamp":1641987969000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7295624\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12]]},"references-count":39,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.1109\/tii.2015.2489184","relation":{},"ISSN":["1551-3203","1941-0050"],"issn-type":[{"value":"1551-3203","type":"print"},{"value":"1941-0050","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12]]}}}