{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T07:49:36Z","timestamp":1771573776653,"version":"3.50.1"},"reference-count":121,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"7","license":[{"start":{"date-parts":[[2019,7,1]],"date-time":"2019-07-01T00:00:00Z","timestamp":1561939200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2019,7,1]],"date-time":"2019-07-01T00:00:00Z","timestamp":1561939200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2019,7,1]],"date-time":"2019-07-01T00:00:00Z","timestamp":1561939200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Ind. Inf."],"published-print":{"date-parts":[[2019,7]]},"DOI":"10.1109\/tii.2019.2908665","type":"journal-article","created":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T18:51:01Z","timestamp":1554144661000},"page":"3772-3783","source":"Crossref","is-referenced-by-count":37,"title":["A Survey of Static Formal Methods for Building Dependable Industrial Automation Systems"],"prefix":"10.1109","volume":"15","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9486-7833","authenticated-orcid":false,"given":"Roopak","family":"Sinha","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2936-4185","authenticated-orcid":false,"given":"Sandeep","family":"Patil","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4299-8270","authenticated-orcid":false,"given":"Luis","family":"Gomes","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9315-9920","authenticated-orcid":false,"given":"Valeriy","family":"Vyatkin","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25942-0_20"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2010.2040393"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2009.2031095"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2016.2634095"},{"key":"ref31","article-title":"An observer-based technique with trace links for requirements validation in embedded real-time systems","author":"zhou","year":"2014"},{"key":"ref30","doi-asserted-by":"crossref","DOI":"10.1145\/3203208","article-title":"TORUS: Scalable requirements traceability for industrial CPS","volume":"3","author":"sinha","year":"2018","journal-title":"ACM Trans Cyber-Physical Systems"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2004.15"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/MAP.2013.6645212"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2008.2008998"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/EFTA.2007.4416832"},{"key":"ref28","first-page":"1","article-title":"Classification of safety requirements for formal verification of software models of industrial automation systems","author":"bitsch","year":"0","journal-title":"Proc Int Conf SW Syst Eng Appl"},{"key":"ref27","first-page":"175","article-title":"A way for applicable formal specification of safety requirements by tool-support","author":"bitsch","year":"0","journal-title":"Proceedings of De-form"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2012.09.011"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.procir.2014.01.140"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.5772\/56412"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2011.2182519"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1504\/IJMR.2007.014730"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/TIE.2017.2682042"},{"key":"ref101","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2015.2489184"},{"key":"ref26","first-page":"1","article-title":"Combining SysML and formal methods for safety requirements verification","author":"p\u00e9tin","year":"0","journal-title":"Proc 22nd Int Conf Softw Syst Eng Appl"},{"key":"ref100","first-page":"911","article-title":"PLCverif: A tool to verify PLC programs based on model checking techniques","author":"darvas","year":"0","journal-title":"Proc 15th Int Conf Accelerator Large Exp Phys Control Syst"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/62.825670"},{"key":"ref50","first-page":"1","article-title":"Multi-formalism based specification language: Syntax, semantics, verification and simulation","volume":"4","author":"mazigh","year":"2014","journal-title":"International Journal of Software Engineering Research & Practices"},{"key":"ref51","first-page":"98","article-title":"Combined synthesis\/verification approach to programmable logic control of a production line","author":"mu\u0161ic","year":"0","journal-title":"Proc 16th IFAC World Congr"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2013.2281733"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2009.2033051"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2017.2670146"},{"key":"ref56","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1504\/IJCAT.2011.045401","article-title":"Virtual start–up of plants using formal methods","volume":"42","author":"preu\u00dfe","year":"2011","journal-title":"Int J Comput Appl Technol"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2005.844433"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1007\/s00170-006-0924-5"},{"key":"ref53","first-page":"197","article-title":"Formal modelling of IEC 61499 function blocks with integer-valued data types","volume":"39","author":"gerber","year":"2010","journal-title":"Control Cybern"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.1997.616302"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2012.2186820"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.arcontrol.2013.09.009"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/TIE.2015.2417501"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.arcontrol.2017.03.004"},{"key":"ref5","author":"kan","year":"2012","journal-title":"Machine Scheduling Problems Classification Complexity and Computations"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0269-9"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.12.115-130"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2014.2345792"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.3182\/20090603-3-RU-2001.0306"},{"key":"ref46","first-page":"22","article-title":"Basic statechart: A formalism to model industrial applications","volume":"1","author":"moura","year":"2010","journal-title":"Model Simul Syst"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1504\/IJIEM.2005.007638"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2011.2169262"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2015.2496262"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1504\/IJISE.2013.056096"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2012.2186585"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-011-0143-6"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2012.2235450"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2000.884359"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2013.27"},{"key":"ref71","first-page":"338","article-title":"Arcade. PLC: A verification platform for programmable logic controllers","author":"biallas","year":"0","journal-title":"Proc 27th IEEE\/ACM Int Conf Automated Softw Eng"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2016.7497884"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2006.355407"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2011.25"},{"key":"ref74","first-page":"198","article-title":"Requirements-aided automatic test-case generation for industrial control software","author":"sinha","year":"0","journal-title":"Proc Int Conf Eng Complex Comput Syst"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1109\/ICARA.2011.6144856"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2009.2039938"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1016\/j.compind.2015.03.007"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2014.09.008"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2017.2710224"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2012.2226578"},{"key":"ref63","first-page":"1","article-title":"Modeling and simulation of IEC 61850 requirements applied to an automated people mover's controller","author":"kunz","year":"0","journal-title":"Proc Int Conf Inf Control Autom Robot"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1109\/COASE.2007.4341688"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1109\/Trustcom.2015.648"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2013.02.061"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1145\/1459352.1459354"},{"key":"ref68","first-page":"7","article-title":"Automatic test-case derivation and execution in industrial control","author":"von styp","year":"0","journal-title":"Proc Workshop Ind Autom Tool Integr Eng Project Autom"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S1474-6670(17)33275-5"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2009.5195890"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-9170-5"},{"key":"ref109","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2011.2116118"},{"key":"ref95","first-page":"7","article-title":"A formal approach for safe controllers analysis","volume":"20","author":"borges","year":"2010","journal-title":"The Romanian Review Precision Mechanics Optics & Mecatronics"},{"key":"ref108","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28959-0_12"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91334-6_18"},{"key":"ref107","doi-asserted-by":"publisher","DOI":"10.1109\/CASE.2011.6042451"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.3182\/20060926-3-PL-4904.00007"},{"key":"ref106","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228484"},{"key":"ref92","doi-asserted-by":"publisher","DOI":"10.1109\/ICCIE.2009.5223968"},{"key":"ref105","doi-asserted-by":"publisher","DOI":"10.1016\/S1474-6670(17)30775-9"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1995.495198"},{"key":"ref104","doi-asserted-by":"publisher","DOI":"10.1109\/Trustcom.2015.650"},{"key":"ref90","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2015.7281905"},{"key":"ref103","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9415-7"},{"key":"ref102","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_32"},{"key":"ref111","doi-asserted-by":"publisher","DOI":"10.1016\/j.matcom.2005.11.010"},{"key":"ref112","doi-asserted-by":"publisher","DOI":"10.1007\/s10845-013-0760-z"},{"key":"ref110","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2010.5641209"},{"key":"ref98","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2013.6622948"},{"key":"ref99","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2001.997677"},{"key":"ref96","doi-asserted-by":"publisher","DOI":"10.1504\/IJMTM.2006.008802"},{"key":"ref97","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_6"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2000.884356"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.4236\/jsea.2015.89048"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1007\/s10270-014-0448-7","article-title":"An overview of model checking practices on verification of PLC software","volume":"15","author":"ovatman","year":"2016","journal-title":"Softw Syst Model"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.23919\/ECC.1999.7099641"},{"key":"ref14","article-title":"A systematic literature review on environment modeling techniques in model-based testing","author":"siavashi","year":"2015"},{"key":"ref15","first-page":"68","volume":"8","author":"petersen","year":"0","journal-title":"Proc 12th Int Conf Eval Assess Softw Eng"},{"key":"ref118","doi-asserted-by":"publisher","DOI":"10.1016\/j.csi.2006.06.002"},{"key":"ref16","first-page":"1","year":"1983","journal-title":"IEEE Standard Glossary of Software Engineering Terminology"},{"key":"ref82","first-page":"670","article-title":"Industrial control systems security: What is happening?","author":"krotofil","year":"0","journal-title":"Proc 11th IEEE Int Conf Ind Inf"},{"key":"ref117","doi-asserted-by":"publisher","DOI":"10.3182\/20080706-5-KR-1001.00856"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-1387-5"},{"key":"ref81","article-title":"Failure mode and effects analysis of software-based automation systems","author":"pentti","year":"2002","journal-title":"VTT Ind Syst STUK-YTO-TR–190"},{"key":"ref18","first-page":"223","article-title":"Formal management of CAD\/CAM processes","author":"kohlhase","year":"2009","journal-title":"Formal Methods"},{"key":"ref84","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2012.05.002"},{"key":"ref119","doi-asserted-by":"publisher","DOI":"10.1016\/S1474-6670(17)36479-0"},{"key":"ref19","article-title":"Innovations for requirements engineering","author":"martell","year":"2008"},{"key":"ref83","doi-asserted-by":"publisher","DOI":"10.1109\/ICCI-CC.2013.6622270"},{"key":"ref114","doi-asserted-by":"publisher","DOI":"10.1109\/WFCS.2006.1704167"},{"key":"ref113","doi-asserted-by":"publisher","DOI":"10.3182\/20130904-3-UK-4041.00015"},{"key":"ref116","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2008.4618113"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1145\/2593783.2593791"},{"key":"ref115","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2014.7005126"},{"key":"ref120","article-title":"Technology readiness levels","volume":"6","author":"mankins","year":"1995"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2016.7733717"},{"key":"ref121","year":"2013","journal-title":"Space Systems - Definition of the Technology Readiness Levels (TRLs) and Their Criteria of Assessment"},{"key":"ref85","doi-asserted-by":"publisher","DOI":"10.3182\/20120523-3-RO-2023.00370"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2015.7081856"},{"key":"ref87","doi-asserted-by":"publisher","DOI":"10.1016\/j.mcm.2011.11.038"},{"key":"ref88","first-page":"41","article-title":"Verifying functional and non-functional properties of manufacturing control systems","author":"preu\u00dfe","year":"0","journal-title":"Proc 3rd Int Workshop Dependable Control Discrete Syst"}],"container-title":["IEEE Transactions on Industrial Informatics"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9424\/8755890\/08678839.pdf?arnumber=8678839","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,13]],"date-time":"2022-07-13T21:02:53Z","timestamp":1657746173000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8678839\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7]]},"references-count":121,"journal-issue":{"issue":"7"},"URL":"https:\/\/doi.org\/10.1109\/tii.2019.2908665","relation":{},"ISSN":["1551-3203","1941-0050"],"issn-type":[{"value":"1551-3203","type":"print"},{"value":"1941-0050","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7]]}}}