{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T15:01:10Z","timestamp":1786978870106,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030374860","type":"print"},{"value":"9783030374877","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-37487-7_5","type":"book-chapter","created":{"date-parts":[[2019,12,13]],"date-time":"2019-12-13T04:22:10Z","timestamp":1576210930000},"page":"50-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Two-Step Deductive Verification of\u00a0Control Software Using Reflex"],"prefix":"10.1007","author":[{"given":"Igor","family":"Anureev","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Natalia","family":"Garanina","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tatiana","family":"Liakh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Rozov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vladimir","family":"Zyubin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sergei","family":"Gorlatch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,12,16]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-35653-0","volume-title":"Diagnosis and Fault-Tolerant Control","author":"M Blanke","year":"2006","unstructured":"Blanke, M., Kinnaert, M., Lunze, J., Staroswiecki, M.: Diagnosis and Fault-Tolerant Control, 2nd edn. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/978-3-540-35653-0","edition":"2"},{"key":"5_CR2","unstructured":"IEC 61131\u20133: Programmable controllers Part 3: Programming languages. Rev. 2.0. International Electrotechnical Commission Standard (2003)"},{"issue":"10","key":"5_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., Gerbasio, D.: On the Implementation of industrial automation systems based on PLC. IEEE Trans. Autom. Sci. Eng. 4(10), 990\u20131003 (2013)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Thramboulidis, K., Frey, G.: An MDD process for IEC 61131-based industrial automation systems. In: 16th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA11), Toulouse, France, pp. 1\u20138 (2011)","DOI":"10.1109\/ETFA.2011.6059118"},{"key":"5_CR5","unstructured":"IEC 61499: Function Blocks for Industrial Process Measurement andControl Systems. Parts 1\u20134. Rev. 1.0. International Electrotechnical Commission Standard (2004\/2005)"},{"key":"5_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., Wolstenholme, P.: Modeling Software with Finite State Machines. Auerbach Publications, Boston (2006)"},{"key":"5_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, 2nd edn. Newnes, Oxford (2009)","edition":"2"},{"key":"5_CR8","unstructured":"Control Technology Corporation. QuickBuilder\u2122Reference Guide (2018). https:\/\/controltechnologycorp.com\/docs\/QuickBuilder_Ref.pdf . Accessed 20 Jan 2019"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Zyubin, V.E.: Hyper-automaton: a model of control algorithms. In: Proceedings of the IEEE International Siberian Conference on Control and Communications (SIBCON-2007), pp. 51\u201357. The Tomsk IEEE Chapter & Student Branch, Tomsk (2007)","DOI":"10.1109\/SIBCON.2007.371297"},{"key":"5_CR10","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Int., Upper Saddle River (1985)"},{"issue":"3","key":"5_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. 8(3), 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"5_CR12","first-page":"219","volume":"2","author":"N Lynch","year":"1989","unstructured":"Lynch, N., Tuttle, M.: An introduction to input\/output automata. CWI Q. 2(3), 219\u2013246 (1989)","journal-title":"CWI Q."},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Berry, G.: The foundations of Esterel. In: Proof, Language and Interaction: Essays in Honour of Robin Milner. Foundations of Computing Series, pp. 425\u2013454. MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0021"},{"key":"5_CR14","series-title":"NATO ASI Series (Series F: Computer and Systems Sciences)","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 170, pp. 265\u2013292. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-642-59615-5_13"},{"key":"5_CR15","series-title":"Series in Computer Science","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Series in Computer Science. Prentice Hall, New Jersey (1989)"},{"key":"5_CR16","unstructured":"Kaynar, D.K., Lynch, N., Segala, R., Vaandrager, F.: Timed I\/O automata: a mathematical framework for modeling and analyzing real-time systems. In: 24th IEEE International Real-Time Systems Symposium (RTSS 2003), pp. 166\u2013177. IEEE Computer Society Cancun, Mexico (2003)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-540-39866-0_34","volume-title":"Perspectives of System Informatics","author":"L Kof","year":"2004","unstructured":"Kof, L., Sch\u00e4tz, B.: Combining aspects of reactive systems. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 344\u2013349. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-39866-0_34"},{"issue":"7","key":"5_CR18","first-page":"36","volume":"2","author":"V Zyubin","year":"1996","unstructured":"Zyubin, V.: SPARM language as a means for programming microcontrollers. Optoelectron. Instr. Data Process. 2(7), 36\u201344 (1996)","journal-title":"Optoelectron. Instr. Data Process."},{"issue":"6","key":"5_CR19","first-page":"85","volume":"12","author":"TV Liakh","year":"2018","unstructured":"Liakh, T.V., Rozov, A.S., Zyubin, V.E.: Reflex language: a practical notation for cyber-physical systems. Syst. Inform. 12(6), 85\u2013104 (2018)","journal-title":"Syst. Inform."},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Rozov A.S., Zyubin V.E.: Process-oriented programming language for MCU-based automation. In: Proceedings of the IEEE International Siberian Conference on Control and Communications, pp. 1\u20134. The Tomsk IEEE Chapter Student Branch, Tomsk (2013)","DOI":"10.1109\/SIBCON.2013.6693595"},{"issue":"5","key":"5_CR21","first-page":"25","volume":"2","author":"D Bulavskij","year":"1996","unstructured":"Bulavskij, D., Zyubin, V., Karlson, N., Krivoruchko, V., Mironov, V.: An automated control system for a silicon single-crystal growth furnace. Optoelectron. Instr. Data Process. 2(5), 25\u201330 (1996)","journal-title":"Optoelectron. Instr. Data Process."},{"key":"5_CR22","volume-title":"LabVIEW for Everyone: Graphical Programming Made Easy and Fun","author":"J Travis","year":"2006","unstructured":"Travis, J., Kring, J.: LabVIEW for Everyone: Graphical Programming Made Easy and Fun, 3rd edn. Prentice Hall PTR, Upper Saddle River (2006)","edition":"3"},{"key":"5_CR23","unstructured":"Zyubin, V.: Using process-oriented programming in LabVIEW. In: Proceedings of the Second IASTED Intern. Multi-Conference on \u201cAutomation, control, and information technology\u201d: Control, Diagnostics, and Automation, Novosibirsk, pp. 35\u201341 (2010)"},{"key":"5_CR24","unstructured":"Randell, B.: Software engineering techniques. Report on a conference sponsored by the NATO Science Committee, p. 16. Brussels, Scientific Affairs Division, NATO, Rome, Italy (1970)"},{"key":"5_CR25","unstructured":"Z3 API in Python. https:\/\/ericpony.github.io\/z3py-tutorial\/guide-examples.htm . Accessed 20 Jan 2019"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"5_CR28","unstructured":"FramaC Homepage. https:\/\/frama-c.com\/"},{"key":"5_CR29","unstructured":"Spark Pro Homepage. https:\/\/www.adacore.com\/sparkpro"},{"key":"5_CR30","unstructured":"The KeY project Homepage https:\/\/www.key-project.org\/"},{"key":"5_CR31","unstructured":"Dafny Homepage. https:\/\/www.microsoft.com\/en-us\/research\/project\/dafny-a-language-and-program-verifier-for-functional-correctness\/"},{"key":"5_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"EW Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/978-1-4612-3228-5"},{"key":"5_CR33","unstructured":"Garanina, N., Zyubin, V., Lyakh, V., Gorlatch, S.: An ontology of specification patterns for verification of concurrent systems. In: New Trends in Intelligent Software Methodologies, Tools and Techniques. Proceedings of the 17th International Conference on SoMeT-18. Series: Frontiers in Artificial Intelligence and Applications, pp. 515\u2013528. IOS Press, Amsterdam (2018)"},{"key":"5_CR34","unstructured":"ACL2 Homepage. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-37487-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,28]],"date-time":"2024-07-28T11:27:28Z","timestamp":1722166048000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-37487-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030374860","9783030374877"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-37487-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"16 December 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PSI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Andrei Ershov Memorial Conference on Perspectives of System Informatics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Novosibirsk","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Russia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ershov2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/psi.nsc.ru\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}