{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:39:15Z","timestamp":1775054355410,"version":"3.50.1"},"reference-count":38,"publisher":"Pleiades Publishing Ltd","issue":"4","license":[{"start":{"date-parts":[[2020,7,1]],"date-time":"2020-07-01T00:00:00Z","timestamp":1593561600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2020,7,1]],"date-time":"2020-07-01T00:00:00Z","timestamp":1593561600000},"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":["Program Comput Soft"],"published-print":{"date-parts":[[2020,7]]},"DOI":"10.1134\/s0361768820040027","type":"journal-article","created":{"date-parts":[[2020,8,8]],"date-time":"2020-08-08T06:02:49Z","timestamp":1596866569000},"page":"261-272","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Dedicative Verification of Reflex Programs"],"prefix":"10.1134","volume":"46","author":[{"given":"I. S.","family":"Anureev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N. O.","family":"Garanina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T. V.","family":"Lyakh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. S.","family":"Rozov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V. E.","family":"Zyubin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S. P.","family":"Gorlatch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"137","published-online":{"date-parts":[[2020,8,8]]},"reference":[{"key":"3519_CR1","volume-title":"Diagnosis and Fault-Tolerant Control","author":"M. Blanke","year":"2006","unstructured":"Blanke, M., Kinnaert, M., Lunze, J., and Staroswiecki, M., Diagnosis and Fault-Tolerant Control, Springer, 2006, 2nd ed."},{"key":"3519_CR2","unstructured":"IEC 61131-3: Programmable controllers, Part 3: Programming languages, Rev. 2.0, International Electrotechnical Commission Std., 2003."},{"key":"3519_CR3","doi-asserted-by":"publisher","first-page":"990","DOI":"10.1109\/TASE.2012.2226578","volume":"4","author":"F. Basile","year":"2013","unstructured":"Basile, F., Chiacchio, P., and Gerbasio, D., On the implementation of industrial automation systems based on PLC, IEEE Trans. Autom. Sci. Eng., 2013, vol. 4, no. 10, pp. 990\u20131003.","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"key":"3519_CR4","doi-asserted-by":"crossref","unstructured":"Thramboulidis, K. and Frey, G., An MDD process for IEC 61131-based industrial automation systems, Proc. 16th IEEE Int. Conf. Emerging Technologies and Factory Automation (ETFA), Toulouse, France, 2011, pp. 1\u20138.","DOI":"10.1109\/ETFA.2011.6059118"},{"key":"3519_CR5","unstructured":"IEC 61499: Function blocks for industrial process measurement and control systems, Parts 1\u20134, Rev. 1.0, International Electrotechnical Commission Std., 2004\u20132005."},{"key":"3519_CR6","doi-asserted-by":"publisher","DOI":"10.1201\/9781420013641","volume-title":"Modeling Software with Finite State Machines","author":"F. Wagner","year":"2006","unstructured":"Wagner, F., Schmuki, R., Wagner, T., and Wolstenholme, P., Modeling Software with Finite State Machines, Boston: Auerbach, 2006."},{"key":"3519_CR7","volume-title":"Practical UML Statecharts in C\/C++: Event-Driven Programming for Embedded Systems","author":"M. Samek","year":"2009","unstructured":"Samek, M., Practical UML Statecharts in C\/C++: Event-Driven Programming for Embedded Systems, Oxford: Newnes, 2009, 2nd ed."},{"key":"3519_CR8","unstructured":"Control Technology Corporation, QuickBuilderTM reference guide, 2018.\nhttps:\/\/controltechnologycorp.com\/docs\/QuickBuilder_Ref.pdf. Accessed January 20, 2019."},{"key":"3519_CR9","doi-asserted-by":"crossref","unstructured":"Zyubin, V.E., Hyper-automaton: A model of control algorithms, Proc. IEEE Int. Sib. Conf. Control and Communications (SIBCON), Tomsk, Russia, 2007, pp. 51\u201357.","DOI":"10.1109\/SIBCON.2007.371297"},{"key":"3519_CR10","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R., Communicating Sequential Processes, Prentice-Hall, 1985."},{"key":"3519_CR11","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D., Statecharts: A visual formalism for complex systems, Sci. Comput. Program., 1987, vol. 8, no. 3, pp.\u00a0231\u2013274.","journal-title":"Sci. Comput. Program."},{"key":"3519_CR12","first-page":"219","volume":"2","author":"N. Lynch","year":"1989","unstructured":"Lynch, N. and Tuttle, M., An introduction to input\/output automata, CWI Quarterly, 1989, vol. 2, no. 3, pp.\u00a0219\u2013246.","journal-title":"CWI Quarterly"},{"key":"3519_CR13","volume-title":"The foundations of Esterel, Proof, Language, and Interaction: Essays in Honour of Robin Milner","author":"G. Berry","year":"2000","unstructured":"Berry, G., The foundations of Esterel, Proof, Language, and Interaction: Essays in Honour of Robin Milner, MIT Press, 2000, pp. 425\u2013454."},{"key":"3519_CR14","volume-title":"The theory of hybrid automata, Verification of Digital and Hybrid Systems, NATO ASI Series (Series F: Computer and Systems Sciences)","author":"T.A. Henzinger","year":"2000","unstructured":"Henzinger, T.A., The theory of hybrid automata, Verification of Digital and Hybrid Systems, NATO ASI Series (Series F: Computer and Systems Sciences), Inan, M.K. and Kurshan, R.P., Eds., Springer, 2000, vol. 170, pp.\u00a0265\u2013292."},{"key":"3519_CR15","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R., Communication and Concurrency, New Jersey: Prentice Hall, 1989."},{"key":"3519_CR16","doi-asserted-by":"crossref","unstructured":"Kaynar, D.K., Lynch, N., Segala, R., and Vaandrager, F., Timed I\/O automata: A mathematical framework for modeling and analyzing real-time systems, Proc. 24th IEEE Int. Real-Time Systems Symp. (RTSS), Cancun, Mexico, 2003, pp. 166\u2013177.","DOI":"10.1109\/REAL.2003.1253264"},{"key":"3519_CR17","unstructured":"Kof, L. and Sch\u00e4tz, B., Combining aspects of reactive systems, Proc. Andrei Ershov 5th Int. Conf. Perspectives of System Informatics, Novosibirsk, 2003, pp. 239\u2013243."},{"key":"3519_CR18","first-page":"36","volume":"2","author":"V. Zyubin","year":"1996","unstructured":"Zyubin, V., SPARM language as a means for programming microcontrollers, Optoelectron., Instrum., Data Process., 1996, vol. 2, no. 7, pp. 36\u201344.","journal-title":"Optoelectron., Instrum., Data Process."},{"key":"3519_CR19","first-page":"85","volume":"12","author":"T.V. Liakh","year":"2018","unstructured":"Liakh, T.V., Rozov, A.S., and Zyubin, V.E., Reflex language: A practical notation for cyber-physical systems, Syst. Inf., 2018, vol. 12, no. 6, pp. 85\u2013104.","journal-title":"Syst. Inf."},{"key":"3519_CR20","doi-asserted-by":"crossref","unstructured":"Rozov, A.S. and Zyubin, V.E., Process-oriented programming language for MCU-based automation, Proc. IEEE Int. Sib. Conf. Control and Communications, Tomsk, Russia, 2013, pp. 1\u20134.","DOI":"10.1109\/SIBCON.2013.6693595"},{"key":"3519_CR21","first-page":"25","volume":"2","author":"D. Bulavskij","year":"1996","unstructured":"Bulavskij, D., Zyubin, V., Karlson, N., Krivoruchko, V., and Mironov, V., An automated control system for a silicon single-crystal growth furnace, Optoelectron., Instrum., Data Process., 1996, vol. 2, no. 5, pp. 25\u201330.","journal-title":"Optoelectron., Instrum., Data Process."},{"key":"3519_CR22","volume-title":"LabVIEW for Everyone: Graphical Programming Made Easy and Fun","author":"J. Travis","year":"2006","unstructured":"Travis, J. and Kring, J., LabVIEW for Everyone: Graphical Programming Made Easy and Fun, New Jersey: Prentice Hall, 2006, 3rd ed."},{"key":"3519_CR23","unstructured":"Zyubin, V., Using process-oriented programming in LabVIEW, Proc. 2nd IASTED Int. Multi-Conf. \u201cAutomation, Control, and Information Technology: Control, Diagnostics, and Automation,\u201d Novosibirsk, 2010, pp. 35\u201341."},{"key":"3519_CR24","volume-title":"Software engineering techniques, Report on a conference sponsored by the NATO Science Committee, Brussels","author":"B. Randell","year":"1970","unstructured":"Randell, B., Software engineering techniques, Report on a conference sponsored by the NATO Science Committee, Brussels, Scientific Affairs Division, NATO, Rome, Italy, 1970, p. 16."},{"key":"3519_CR25","unstructured":"Z3 API in Python. https:\/\/ericpony.github.io\/z3py-tutorial\/guide-examples.htm. Accessed January 20, 2019."},{"key":"3519_CR26","doi-asserted-by":"crossref","unstructured":"Moura, L. and Bj\u00f8rner, N., Z3: An efficient SMT solver, Proc. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lect. Notes Comput. Sci., 2008, vol. 4963, pp. 337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"3519_CR27","doi-asserted-by":"crossref","unstructured":"Anureev, I.S., Garanina, N.O., Liakh, T.V., Rozov, A.S., Zyubin, V.E., and Gorlatch, S., Two-step deductive verification of control software using Reflex, Proc. A.P. Ershov Informatics Conference (PSI), Novosibirsk, Russia, Lect. Notes Comput. Sci., 2019, vol. 11964, pp. 50\u201363.","DOI":"10.1007\/978-3-030-37487-7_5"},{"key":"3519_CR28","doi-asserted-by":"crossref","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., and Leino, K.R.M., Boogie: A modular reusable verifier for object-oriented programs, Proc. 4th Int. Conf. Formal Methods for Components and Objects, Lect. Notes Comput. Sci., 2005, vol. 4111, pp. 364\u2013387.","DOI":"10.1007\/11804192_17"},{"key":"3519_CR29","unstructured":"FramaC homepage. https:\/\/frama-c.com."},{"key":"3519_CR30","unstructured":"Spark Pro homepage. https:\/\/www.adacore.com\/ sparkpro."},{"key":"3519_CR31","unstructured":"The KeY project homepage. https:\/\/www.key-project.org."},{"key":"3519_CR32","unstructured":"Dafny homepage. https:\/\/www.microsoft.com\/en-us\/research\/project\/dafny-a-language-and-program-verifier-for-functional-correctness."},{"key":"3519_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"Dijkstra, E.W. and Scholten, C.S., Predicate Calculus and Program Semantics, Springer, 1990."},{"key":"3519_CR34","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1023\/A:1021045909505","volume":"28","author":"V. Nepomniaschy","year":"2002","unstructured":"Nepomniaschy, V., Anureev, I., Mikhailov, I., and Promsky, A., Towards verification of C programs: C\u2011light language and its formal semantics, Program. Comput. Software, 2002, vol. 28, no. 6, pp. 314\u2013323.","journal-title":"Program. Comput. Software"},{"key":"3519_CR35","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1023\/B:PACS.0000004134.24714.e5","volume":"29","author":"V. Nepomniaschy","year":"2003","unstructured":"Nepomniaschy, V., Anureev, I., and Promsky, A., Towards verification of C programs: Axiomatic semantics of the C-kernel language, Program. Comput. Software, 2003, vol. 29, no. 6, pp. 338\u2013350.","journal-title":"Program. Comput. Software"},{"key":"3519_CR36","unstructured":"Garanina, N., Zyubin, V., Lyakh, V., and Gorlatch, S., An ontology of specification patterns for verification of concurrent systems, New Trends in Intelligent Software Methodologies, Tools, and Techniques (Proc. 17th Int. Conf. SoMeT), Series: Frontiers in Artificial Intelligence and Applications, Amsterdam: IOS Press, 2018, pp. 515\u2013528."},{"key":"3519_CR37","unstructured":"ACL2 homepage. http:\/\/www.cs.utexas.edu\/users\/ moore\/acl2."},{"key":"3519_CR38","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1134\/S0361768809010058","volume":"35","author":"I.S. Anureev","year":"2009","unstructured":"Anureev, I.S., Operational ontological approach to formal programming language specification, Program. Comput. Software, 2009, vol. 35, no. 1, pp. 35\u201342.","journal-title":"Program. Comput. Software"}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768820040027.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1134\/S0361768820040027","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768820040027.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T02:45:29Z","timestamp":1775011529000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1134\/S0361768820040027"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020,7]]}},"alternative-id":["3519"],"URL":"https:\/\/doi.org\/10.1134\/s0361768820040027","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,7]]},"assertion":[{"value":"10 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 February 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 August 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}