{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:58:52Z","timestamp":1773615532930,"version":"3.50.1"},"reference-count":33,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2024,12,1]],"date-time":"2024-12-01T00:00:00Z","timestamp":1733011200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,12,1]],"date-time":"2024-12-01T00:00:00Z","timestamp":1733011200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Control Comp. Sci."],"published-print":{"date-parts":[[2024,12]]},"DOI":"10.3103\/s0146411624700433","type":"journal-article","created":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T14:48:33Z","timestamp":1739371713000},"page":"1025-1041","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking Programs in Process-Oriented IEC 61131-3 Structured Text"],"prefix":"10.3103","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9734-3808","authenticated-orcid":false,"given":"N. O.","family":"Garanina","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5183-9736","authenticated-orcid":false,"given":"S. M.","family":"Staroletov","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8198-3197","authenticated-orcid":false,"given":"V. E.","family":"Zyubin","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9574-128X","authenticated-orcid":false,"given":"I. S.","family":"Anureev","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2025,2,12]]},"reference":[{"key":"7764_CR1","unstructured":"IEC (International Standard) 61131-3: 2013 Programmable controllers, part 3: Programming languages, 2013. https:\/\/webstore.iec.ch\/publication\/4552."},{"key":"7764_CR2","volume-title":"PLC Controls with Structured Text (ST), V3: IEC 61131-3 and Best Practice ST Programming","author":"T.M. Antonsen","year":"2020","unstructured":"Antonsen, T.M., PLC Controls with Structured Text (ST), V3: IEC 61131-3 and Best Practice ST Programming, Books on Demand, 2020."},{"key":"7764_CR3","doi-asserted-by":"publisher","unstructured":"Zyubin, V.E., Hyper-automaton: A model of control algorithms, 2007 Siberian Conf. on Control and Communications, Tomsk, 2007, IEEE, 2007, pp. 51\u201357. https:\/\/doi.org\/10.1109\/sibcon.2007.371297","DOI":"10.1109\/sibcon.2007.371297"},{"key":"7764_CR4","doi-asserted-by":"publisher","first-page":"35238","DOI":"10.1109\/access.2022.3157601","volume":"10","author":"V.E. Zyubin","year":"2022","unstructured":"Zyubin, V.E., Rozov, A.S., Anureev, I.S., Garanina, N.O., and Vyatkin, V., poST: A process-oriented extension of the IEC 61131-3 structured text language, IEEE Access, 2022, vol. 10, pp. 35238\u201335250. https:\/\/doi.org\/10.1109\/access.2022.3157601","journal-title":"IEEE Access"},{"key":"7764_CR5","volume-title":"The SPIN Model Checker, Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J., The SPIN Model Checker, Primer and Reference Manual, Reading, Mass.: Addison-Wesley, 2003."},{"key":"7764_CR6","doi-asserted-by":"publisher","unstructured":"Schneider, L. and Schultes, D., Evaluating Swift-to-Kotlin and Kotlin-to-Swift transpilers, Proc. 9th\u00a0IEEE\/ACM Int. Conf. on Mobile Software Engineering and Systems, Pittsburgh, Pa., 2022, New York: Association for Computing Machinery, 2022, pp. 102\u2013106. https:\/\/doi.org\/10.1145\/3524613.3527811","DOI":"10.1145\/3524613.3527811"},{"key":"7764_CR7","doi-asserted-by":"publisher","unstructured":"Handbook of Model Checking, Clarke, E.M., Henzinger, T.A., Veith, H., and Bloem, R., Eds., Cham: Springer, 2018. https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"7764_CR8","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1007\/s10270-014-0448-7","volume":"15","author":"T. Ovatman","year":"2016","unstructured":"Ovatman, T., Aral, A., Polat, D., and \u00dcnver, A.O., An overview of model checking practices on verification of PLC software, Software Syst. Model., 2016, vol. 15, no. 4, pp. 937\u2013960. https:\/\/doi.org\/10.1007\/s10270-014-0448-7","journal-title":"Software Syst. Model."},{"key":"7764_CR9","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., and Sistla, A.P., Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang.s Syst., 1986, vol. 8, no. 2, pp. 244\u2013263. https:\/\/doi.org\/10.1145\/5397.5399","journal-title":"ACM Trans. Program. Lang.s Syst."},{"key":"7764_CR10","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"Hoare, C.A.R., Communicating sequential processes, Commun. ACM, 1978, vol. 21, no. 8, pp. 666\u2013677. https:\/\/doi.org\/10.1145\/359576.359585","journal-title":"Commun. ACM"},{"key":"7764_CR11","doi-asserted-by":"publisher","first-page":"21","DOI":"10.31144\/si.2307-6410.2023.n22.p21-30","volume":"22","author":"N. Garanina","year":"2023","unstructured":"Garanina, N., Staroletov, S., Zyubin, V., and Anureev, I., Model checking process-oriented iec 61131-3 structured text programs, Syst. Inf., 2023, vol. 22, no. 22, pp. 21\u201330. https:\/\/doi.org\/10.31144\/si.2307-6410.2023.n22.p21-30","journal-title":"Syst. Inf."},{"key":"7764_CR12","doi-asserted-by":"publisher","unstructured":"Wei\u00dfmann, M., Bedenk, S., Buckl, Ch., and Knoll, A., Model checking industrial robot systems, Model Checking Software, Groce, A. and Musuvathi, M., Eds., Lecture Notes in Computer Science, vol. 6823, Berlin: Springer, 2011, pp. 161\u2013176. https:\/\/doi.org\/10.1007\/978-3-642-22306-8_11","DOI":"10.1007\/978-3-642-22306-8_11"},{"key":"7764_CR13","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1145\/234528.234740","volume":"28","author":"P. Cousot","year":"1996","unstructured":"Cousot, P., Abstract interpretation, ACM Comput. Surv., 1996, vol. 28, no. 2, pp. 324\u2013328. https:\/\/doi.org\/10.1145\/234528.234740","journal-title":"ACM Comput. Surv."},{"key":"7764_CR14","doi-asserted-by":"publisher","unstructured":"Leue, S. and Holzmann, G., v-Promela: A visual, object-oriented language for SPIN, Proc. 2nd IEEE Int. Symp. on Object-Oriented Real-Time Distributed Computing (ISORC\u201999), Saint-Malo, France, 1999, IEEE, 1999, pp.\u00a014\u201323. https:\/\/doi.org\/10.1109\/isorc.1999.776345","DOI":"10.1109\/isorc.1999.776345"},{"key":"7764_CR15","doi-asserted-by":"publisher","unstructured":"Benerecetti, M., Gentile, U., Marrone, S., Nardone, R., Peron, A., Starace, L.L.L., and Vittorini, V., From dynamic state machines to Promela, Model Checking Software, Biondi, F., Given-Wilson, T., and Legay, A., Eds., Lecture Notes in Computer Science, vol. 11636, Cham: Springer, 2019, pp. 56\u201373. https:\/\/doi.org\/10.1007\/978-3-030-30923-7_4","DOI":"10.1007\/978-3-030-30923-7_4"},{"key":"7764_CR16","first-page":"31","volume":"2245","author":"B. Lion","year":"2018","unstructured":"Lion, B., Chouali, S., and Arbab, F., Compiling protocols to Promela and verifying their LTL properties, CEUR Workshop Proc., 2018, vol. 2245, pp. 31\u201339. https:\/\/ir.cwi.nl\/pub\/28464\/modcomp_paper_5.pdf.","journal-title":"CEUR Workshop Proc."},{"key":"7764_CR17","doi-asserted-by":"publisher","unstructured":"Klarl, A., From Helena ensemble specifications to Promela verification models, Model Checking Software, Fischer, B. and Geldenhuys, J., Eds., Lecture Notes in Computer Science, vol. 9232, Cham: Springer, 2015, pp. 39\u201345. https:\/\/doi.org\/10.1007\/978-3-319-23404-5_4","DOI":"10.1007\/978-3-319-23404-5_4"},{"key":"7764_CR18","doi-asserted-by":"publisher","first-page":"34","DOI":"10.4204\/eptcs.314.4","volume":"314","author":"N. Dilley","year":"2010","unstructured":"Dilley, N. and Lange, J., Bounded verification of message-passing concurrency in Go using Promela and Spin, Electron. Proc. Theor. Comput. Sci., 2010, vol. 314, pp. 34\u201345. https:\/\/doi.org\/10.4204\/eptcs.314.4","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"7764_CR19","doi-asserted-by":"publisher","unstructured":"Dilley, N. and Lange, J., Automated verification of Go programs via bounded model checking, 2021 36th\u00a0IEEE\/ACM Int. Conf. on Automated Software Engineering (ASE), Melbourne, Australia, 2021, IEEE, 2021, pp. 1016\u20131027. https:\/\/doi.org\/10.1109\/ase51524.2021.9678571","DOI":"10.1109\/ase51524.2021.9678571"},{"key":"7764_CR20","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10009-002-0079-0","volume":"4","author":"E. Brinksma","year":"2002","unstructured":"Brinksma, E., Mader, A., and Fehnker, A., Verification and optimization of a PLC control schedule, Int. J. Software Tools Technol. Transfer, 2002, vol. 4, no. 1, pp. 21\u201333. https:\/\/doi.org\/10.1007\/s10009-002-0079-0","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"7764_CR21","doi-asserted-by":"publisher","unstructured":"Xia, M., Sun, M., Luo, G., and Zhao, X., Design and implementation of automatic verification for PLC systems, 2013 IEEE 12th Int. Conf. on Cognitive Informatics and Cognitive Computing, New York, 2013, IEEE, 2013, pp. 374\u2013379. https:\/\/doi.org\/10.1109\/icci-cc.2013.6622270","DOI":"10.1109\/icci-cc.2013.6622270"},{"key":"7764_CR22","doi-asserted-by":"publisher","unstructured":"Liu, P., Luo, G., Xia, M., and He, M., Automatic verification of event-driven control programs: A case study, The Fourth Int. Workshop on Advanced Computational Intell., Wuhan, China, 2011, IEEE, 2011, pp. 249\u2013256. https:\/\/doi.org\/10.1109\/iwaci.2011.6160012","DOI":"10.1109\/iwaci.2011.6160012"},{"key":"7764_CR23","doi-asserted-by":"publisher","unstructured":"Liakh, T., Sorokin, R., Akifev, D., Patil, S., and Vyatkin, V., Formal model of IEC 61499 execution trace in FBME IDE, 2022 IEEE 20th Int. Conf. on Industrial Informatics (INDIN), Perth, Australia, 2022, IEEE, 2022, pp. 588\u2013593. https:\/\/doi.org\/10.1109\/indin51773.2022.9976176","DOI":"10.1109\/indin51773.2022.9976176"},{"key":"7764_CR24","doi-asserted-by":"publisher","unstructured":"Shatrov, V. and Vyatkin, V., Promela formal modelling and verification of IEC 61499 systems with comparison to SMV, 2021 IEEE 19th Int. Conf. on Industrial Informatics (INDIN), Palma de Mallorca, Spain, 2021, IEEE, 2021, pp. 1\u20136. https:\/\/doi.org\/10.1109\/indin45523.2021.9557513","DOI":"10.1109\/indin45523.2021.9557513"},{"key":"7764_CR25","volume-title":"Formalizing ladder logic programs and timing charts for fault impact analysis and verification of fault tolerance, Tech. Rep. CS-TR-23-01","author":"A. Ebnenasir","year":"2023","unstructured":"Ebnenasir, A., Formalizing ladder logic programs and timing charts for fault impact analysis and verification of fault tolerance, Tech. Rep. CS-TR-23-01, Houghton, Mich.: Michigan Technological Univ., 2023.\nhttps:\/\/www.mtu.edu\/cs\/research\/papers\/pdfs\/formalizing-ladder-logic-ali-ebnenasir-tech-rpt-010623-rev.pdf."},{"key":"7764_CR26","doi-asserted-by":"publisher","unstructured":"Mader, A., A classification of PLC models and applications, Discrete Event Systems, Boel, R. and Stremersch, G., Eds., The Springer International Series in Engineering and Computer Science, vol. 569, Boston: Springer, 2000, pp. 239\u2013246. https:\/\/doi.org\/10.1007\/978-1-4615-4493-7_24","DOI":"10.1007\/978-1-4615-4493-7_24"},{"key":"7764_CR27","doi-asserted-by":"publisher","first-page":"763","DOI":"10.3103\/s0146411621070038","volume":"55","author":"N.O. Garanina","year":"2021","unstructured":"Garanina, N.O., Anureev, I.S., Zyubin, V.E., Staroletov, S.M., Liakh, T.V., Rozov, A.S., and Gorlatch, S.P., A\u00a0temporal logic for programmable logic controllers, Autom. Control Comput. Sci., 2021, vol. 55, no. 7, pp. 763\u2013775. https:\/\/doi.org\/10.3103\/s0146411621070038","journal-title":"Autom. Control Comput. Sci."},{"key":"7764_CR28","doi-asserted-by":"publisher","unstructured":"Eysholdt, M. and Behrens, H., Xtext: Implement your language faster than the quick and dirty way, Proc. of the ACM Int. Conf. Companion on Object Oriented Programming Systems Languages and Applications Companion, Reno, Nev., 2010, New York: Association for Computing Machinery, 2010, pp. 307\u2013309. https:\/\/doi.org\/10.1145\/1869542.1869625","DOI":"10.1145\/1869542.1869625"},{"key":"7764_CR29","volume-title":"EMF: Eclipse Modeling Framework","author":"D. Steinberg","year":"2008","unstructured":"Steinberg, D., Budinsky, F., Paternostro, M., and Merks, E., EMF: Eclipse Modeling Framework, Upper Saddle River, N.J.: Addison-Wesley, 2008, 2nd ed."},{"key":"7764_CR30","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1002\/spe.4380250705","volume":"25","author":"T.J. Parr","year":"1995","unstructured":"Parr, T.J. and Quong, R.W., ANTLR: A predicated-LL (k) parser generator, Software: Pract. Exper., 1995, vol.\u00a025, no. 7, pp. 789\u2013810. https:\/\/doi.org\/10.1002\/spe.4380250705","journal-title":"Software: Pract. Exper."},{"key":"7764_CR31","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1016\/j.scico.2014.06.006","volume":"99","author":"D. Lepri","year":"2015","unstructured":"Lepri, D., \u00c1brah\u00e1m, E., and \u00d6lveczky, P.C., Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories, Sci. Comput. Program., 2015, vol. 99, pp. 128\u2013192. https:\/\/doi.org\/10.1016\/j.scico.2014.06.006","journal-title":"Sci. Comput. Program."},{"key":"7764_CR32","volume-title":"Palm OS Programming: The Developer\u2019s Guide","author":"N. Rhodes","year":"2002","unstructured":"Rhodes, N. and McKeehan, J., Palm OS Programming: The Developer\u2019s Guide, O\u2019Reilly Media, 2002."},{"key":"7764_CR33","volume-title":"Learning UML 2.0: A Pragmatic Introduction to UML","author":"R. Miles","year":"2006","unstructured":"Miles, R. and Hamilton, K., Learning UML 2.0: A Pragmatic Introduction to UML, O\u2019Reilly Media, 2006."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411624700433.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411624700433","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411624700433.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:01:14Z","timestamp":1773612074000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411624700433"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12]]},"references-count":33,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["7764"],"URL":"https:\/\/doi.org\/10.3103\/s0146411624700433","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12]]},"assertion":[{"value":"17 January 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 February 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 February 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 February 2025","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors of this work declare that they have no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}