{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T23:01:27Z","timestamp":1773615687923,"version":"3.50.1"},"reference-count":31,"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\/s0146411624700421","type":"journal-article","created":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T14:48:31Z","timestamp":1739371711000},"page":"1003-1024","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Requirement Patterns in Deductive Verification of poST Programs"],"prefix":"10.3103","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7675-8449","authenticated-orcid":false,"given":"I. M.","family":"Chernenko","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9574-128X","authenticated-orcid":false,"given":"I. S.","family":"Anureev","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9734-3808","authenticated-orcid":false,"given":"N. O.","family":"Garanina","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2025,2,12]]},"reference":[{"key":"7763_CR1","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":"7763_CR2","doi-asserted-by":"publisher","unstructured":"Anureev, I., Garanina, N., Liakh, T., Rozov, A., Zyubin, V., and Gorlatch, S., Two-step deductive verification of control software using Reflex, Perspectives of System Informatics. PSI 2019, Bj\u00f8rner, N., Virbitskaite, I., and Voronkov, A., Eds., Lecture Notes in Computer Science, vol. 11964, Cham: Springer, 2019, pp. 50\u201363. https:\/\/doi.org\/10.1007\/978-3-030-37487-7_5","DOI":"10.1007\/978-3-030-37487-7_5"},{"key":"7763_CR3","doi-asserted-by":"publisher","unstructured":"Zyubin, V., Liakh, T., and Rozov, A., Reflex language: A practical notation for cyber-physical systems, Syst. Inf., 2018, no. 12, pp. 85\u2013104. https:\/\/doi.org\/10.31144\/si.2307-6410.2018.n12.p85-104","DOI":"10.31144\/si.2307-6410.2018.n12.p85-104"},{"key":"7763_CR4","doi-asserted-by":"publisher","unstructured":"Paulin-Mohring, C., Introduction to the Coq proof-assistant for practical software verification, Tools for Practical Software Verification. LASER 2011, Meyer, B. and Nordio, M., Eds., Lecture Notes in Computer Science, vol. 7682, Berlin: Springer, 2011, pp. 45\u201395. https:\/\/doi.org\/10.1007\/978-3-642-35746-63","DOI":"10.1007\/978-3-642-35746-63"},{"key":"7763_CR5","doi-asserted-by":"publisher","unstructured":"Chernenko, I., Anureev, I.S., Garanina, N.O., and Staroletov, S.M., A temporal requirements language for deductive verification of process-oriented programs, 2022 IEEE 23rd Int. Conf. of Young Professionals in Electron Devices and Materials (EDM), Altai, 2022, IEEE, 2022, pp. 657\u2013662. https:\/\/doi.org\/10.1109\/edm55285.2022.9855145","DOI":"10.1109\/edm55285.2022.9855145"},{"key":"7763_CR6","doi-asserted-by":"publisher","unstructured":"Chernenko, I.M. and Anureev, I.S., Development of verification condition generator for process-oriented programs in PoST language, 2023 IEEE 24th Int. Conf. of Young Professionals in Electron Devices and Materials (EDM), Novosibirsk, 2023, IEEE, 2023, pp. 1760\u20131765. https:\/\/doi.org\/10.1109\/edm58354.2023.10225217","DOI":"10.1109\/edm58354.2023.10225217"},{"key":"7763_CR7","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":"7763_CR8","unstructured":"IEC (International Standard) 61131-3: 2013 programmable controllers, part 3: Programming languages, 2013. https:\/\/webstore.iec.ch\/publication\/4552."},{"key":"7763_CR9","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/s00165-019-00492-1","volume":"31","author":"L.C. Paulson","year":"2019","unstructured":"Paulson, L.C., Nipkow, T., and Wenzel, M., From LCF to Isabelle\/HOL, Formal Aspects Comput., 2019, vol.\u00a031, no. 6, pp. 675\u2013698. https:\/\/doi.org\/10.1007\/s00165-019-00492-1","journal-title":"Formal Aspects Comput."},{"key":"7763_CR10","doi-asserted-by":"publisher","unstructured":"Chernenko, I., Requirements patterns in deductive verification of process-oriented programs and examples of their use, Syst. Inf., 2023, no. 22, pp. 11\u201320. https:\/\/doi.org\/10.31144\/si.2307-6410.2023.n22.p11-20","DOI":"10.31144\/si.2307-6410.2023.n22.p11-20"},{"key":"7763_CR11","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-011-0211-0","volume":"13","author":"J.-C. Filli\u00e2tre","year":"2011","unstructured":"Filli\u00e2tre, J.-C., Deductive software verification, Int. J. Software Tools Technol. Transfer, 2011, vol. 13, no. 5, pp.\u00a0397\u2013403. https:\/\/doi.org\/10.1007\/s10009-011-0211-0","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"7763_CR12","doi-asserted-by":"publisher","unstructured":"Gurov, D., Herber, P., and Schaefer, I., Automated verification of embedded control software, Leveraging Applications of Formal Methods, Verification and Validation: Applications. ISoLA 2020, Margaria, T. and Steffen, B., Eds., Lecture Notes in Computer Science, vol. 12478, Cham: Springer, 2020, pp. 235\u2013239. https:\/\/doi.org\/10.1007\/978-3-030-61467-615","DOI":"10.1007\/978-3-030-61467-615"},{"key":"7763_CR13","doi-asserted-by":"publisher","unstructured":"Gurov, D., Lidstr\u00f6m, Ch., Nyberg, M., and Westman, J., Deductive functional verification of safety-critical embedded C-code: An experience report, Critical Systems: Formal Methods and Automated Verification. AVoCS FMICS 2017, Petrucci, L., Seceleanu, C., and Cavalcanti, A., Eds., Lecture Notes in Computer Science, vol.\u00a010471, Cham: Springer, 2017, pp. 3\u201318. https:\/\/doi.org\/10.1007\/978-3-319-67113-0_1","DOI":"10.1007\/978-3-319-67113-0_1"},{"key":"7763_CR14","doi-asserted-by":"publisher","unstructured":"Louren\u00e7o, C.B., Cousineau, D., Faissole, F., March\u00e9, C., Mentr\u00e9, D., and Inoue, H., Automated verification of temporal properties of ladder programs, Formal Methods for Industrial Critical Systems, Lluch Lafuente, A. and Mavridou, A., Eds., Lecture Notes in Computer Science, Cham: Springer, 2021, pp. 21\u201338. https:\/\/doi.org\/10.1007\/978-3-030-85248-1_2","DOI":"10.1007\/978-3-030-85248-1_2"},{"key":"7763_CR15","doi-asserted-by":"publisher","unstructured":"Manna, Z., Bj\u00f8rner, N.S., Browne, A., Col\u00f3n, M., Finkbeiner, B., Pichora, M., Sipma, H.B., and Uribe, T.E., An update on STeP: Deductive-algorithmic verification of reactive systems, Tool Support for System Specification, Development and Verification, Berghammer, R. and Lakhnech, Y., Eds., Advances in Computing Science, Vienna: Springer, 1999, pp. 174\u2013188. https:\/\/doi.org\/10.1007\/978-3-7091-6355-913","DOI":"10.1007\/978-3-7091-6355-913"},{"key":"7763_CR16","doi-asserted-by":"publisher","first-page":"1163","DOI":"10.3390\/electronics8101163","volume":"8","author":"S. Yamane","year":"2019","unstructured":"Yamane, S., Deductive verification method of real-time safety properties for embedded assembly programs, Electronics, 2019, vol. 8, no. 10, p. 1163. https:\/\/doi.org\/10.3390\/electronics8101163","journal-title":"Electronics"},{"key":"7763_CR17","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":"7763_CR18","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 temporal 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":"7763_CR19","doi-asserted-by":"publisher","unstructured":"Manna, Z. and Pnueli, A., The Temporal Logic of Reactive and Concurrent Systems, New York: Springer, 1992. https:\/\/doi.org\/10.1007\/978-1-4612-0931-7","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"7763_CR20","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Avrunin, G.S., and Corbett, J.C., Patterns in property specifications for finite-state verification, Proc. 21st Int. Conf. on Software Engineering, Los Angeles, 1999, New York: Association for Computing Machinery, 1999, pp. 411\u2013420. https:\/\/doi.org\/10.1145\/302405.302672","DOI":"10.1145\/302405.302672"},{"key":"7763_CR21","doi-asserted-by":"publisher","unstructured":"Grunske, L., Specification patterns for probabilistic quality properties, Proc. 13th Int. Conf. on Software Engineering\u2013ICSE \u201908, Leipzig, Germany, 2008, New York: Association for Computing Machinery, 2008, pp. 31\u201340. https:\/\/doi.org\/10.1145\/1368088.1368094","DOI":"10.1145\/1368088.1368094"},{"key":"7763_CR22","doi-asserted-by":"publisher","unstructured":"Konrad, S. and Cheng, B.H.C., Real-time specification patterns, Proc. 27th Int. Conf. on Software Engineering\u2013ICSE \u201905, St. Louis, Mo., 2005, New York: Association for Computing Machinery, 2005, pp. 372\u2013381. https:\/\/doi.org\/10.1145\/1062455.1062526","DOI":"10.1145\/1062455.1062526"},{"key":"7763_CR23","first-page":"47","volume":"3","author":"A. Mekki","year":"2012","unstructured":"Mekki, A., Ghazel, M., and Toguy\u00e9ni, A., Assisting temporal requirement specification, Comput. Technol. Appl., 2012, vol. 3, no. 1, pp. 47\u201355.","journal-title":"Comput. Technol. Appl."},{"key":"7763_CR24","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/S1571-0661(04)81043-0","volume":"89","author":"O. Mondragon","year":"2003","unstructured":"Mondragon, O., Gates, A.Q., and Roach, S., Prospec: Support for elicitation and formal specification of software properties, Electron. Notes Theor. Comput. Sci., 2003, vol. 89, no. 2, pp. 67\u201388. https:\/\/doi.org\/10.1016\/S1571-0661(04)81043-0","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"7763_CR25","doi-asserted-by":"publisher","first-page":"1915","DOI":"10.1016\/j.jss.2012.02.041","volume":"85","author":"S. Salamah","year":"2012","unstructured":"Salamah, S., Gates, A., and Kreinovich, V., Validated templates for specification of complex LTL formulas, J.\u00a0Syst. Software, 2012, vol. 85, no. 8, pp. 1915\u20131929. https:\/\/doi.org\/10.1016\/j.jss.2012.02.041","journal-title":"J.\u00a0Syst. Software"},{"key":"7763_CR26","doi-asserted-by":"publisher","unstructured":"Bianculli, D., Ghezzi, C., Pautasso, C., and Senti, P., Specification patterns from research to industry: A case study in service-based applications, 2012 34th Int. Conf. on Software Engineering (ICSE), Zurich, 2012, IEEE, 2012, pp. 968\u2013976. https:\/\/doi.org\/10.1109\/icse.2012.6227125","DOI":"10.1109\/icse.2012.6227125"},{"key":"7763_CR27","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1109\/tse.2009.29","volume":"35","author":"S. Halle","year":"2009","unstructured":"Halle, S., Villemaire, R., and Cherkaoui, O., Specifying and validating data-aware temporal web service properties, IEEE Trans. Software Eng., 2009, vol. 35, no. 5, pp. 669\u2013683. https:\/\/doi.org\/10.1109\/tse.2009.29","journal-title":"IEEE Trans. Software Eng."},{"key":"7763_CR28","doi-asserted-by":"publisher","unstructured":"Post, A., Menzel, I., and Podelski, A., Applying restricted english grammar on automotive requirements\u2014Does it work? A case study, Requirements Engineering: Foundation for Software Quality, Berry, D. and Franch, X., Eds., Lecture Notes in Computer Science, vol. 6606, Berlin: Springer, 2011, pp. 166\u2013180. https:\/\/doi.org\/10.1007\/978-3-642-19858-8_17","DOI":"10.1007\/978-3-642-19858-8_17"},{"key":"7763_CR29","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1109\/tse.2015.2398877","volume":"41","author":"M. Autili","year":"2015","unstructured":"Autili, M., Grunske, L., Lumpe, M., Pelliccione, P., and Tang, A., Aligning qualitative, real-time, and probabilistic property specification patterns using a structured English grammar, IEEE Trans. Software Eng., 2015, vol. 41, no. 7, pp. 620\u2013638. https:\/\/doi.org\/10.1109\/tse.2015.2398877","journal-title":"IEEE Trans. Software Eng."},{"key":"7763_CR30","doi-asserted-by":"publisher","unstructured":"Getmanova, A.N., Garanina, N.O., Staroletov, S.M., Zyubin, V.E., and Anureev, I.S., Semantic classification of event driven temporal logic requirements, 2022 IEEE 23rd Int. Conf. of Young Professionals in Electron Devices and Materials (EDM), Altai, 2022, IEEE, 2022, pp. 663\u2013668. https:\/\/doi.org\/10.1109\/edm55285.2022.9855053","DOI":"10.1109\/edm55285.2022.9855053"},{"key":"7763_CR31","doi-asserted-by":"publisher","unstructured":"Zyubin, V., Anureev, I., Garanina, N., Staroletov, S., Rozov, A., and Liakh, T., Event-driven temporal logic pattern for control software requirements specification, Fundamentals of Software Engineering, Hojjat, H. and Massink, M., Eds., Lecture Notes in Computer Science, vol. 12818, Cham: Springer, 2021, pp. 92\u2013107. https:\/\/doi.org\/10.1007\/978-3-030-89247-0_7","DOI":"10.1007\/978-3-030-89247-0_7"}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411624700421.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411624700421","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411624700421.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:03:20Z","timestamp":1773612200000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411624700421"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12]]},"references-count":31,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["7763"],"URL":"https:\/\/doi.org\/10.3103\/s0146411624700421","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":"12 January 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 February 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 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"}}]}}