{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:55:09Z","timestamp":1767138909581,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319259413","type":"print"},{"value":"9783319259420","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","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":[[2015]]},"DOI":"10.1007\/978-3-319-25942-0_20","type":"book-chapter","created":{"date-parts":[[2015,10,16]],"date-time":"2015-10-16T05:32:14Z","timestamp":1444973534000},"page":"300-315","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Formal Modelling and Verification of IEC61499 Function Blocks with Abstract State Machines and SMV - Execution Semantics"],"prefix":"10.1007","author":[{"given":"Sandeep","family":"Patil","sequence":"first","affiliation":[]},{"given":"Victor","family":"Dubinin","sequence":"additional","affiliation":[]},{"given":"Victor","family":"Vyatkin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,17]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"768","DOI":"10.1109\/TII.2011.2166785","volume":"7","author":"V Vyatkin","year":"2011","unstructured":"Vyatkin, V.: IEC 61499 as Enabler of Distributed and Intelligent Automation: State-of-the-Art Review. IEEE Transactions on Industrial Informatics 7, 768\u2013781 (2011)","journal-title":"IEEE Transactions on Industrial Informatics"},{"key":"20_CR2","unstructured":"Function blocks\u2014 Part 1: Architecture, IEC Standard 61499-1, Second ed. (2012)"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Patil, S., Dubinin, V., Pang, C.,Vyatkin, V.: Neutralizing semantic ambiguities of function block architecture by modeling with ASM. In: 9th International Andrei Ershov Memorial Conference, PSI 2014 PeterhofSt. Petersburg, Russia (2014)","DOI":"10.1007\/978-3-662-46823-4_7"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Patil, S.,Dubinin, V.,yatkin, VV.: Formal verification of IEC61499 function blocks with abstract state machines and smv \u2013 modelling. In: The 13th IEEE International Symposium on Parallel and Distributed Processing with Applications (IEEE ISPA-15) Helsinki, Finland (2015)","DOI":"10.1109\/Trustcom.2015.650"},{"key":"20_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1155\/2008\/426713","volume":"2008","author":"V Dubinin","year":"2008","unstructured":"Dubinin, V., Vyatkin, V.: On definition of a formal model for IEC 61499 function blocks. EURASIP Journal on Embedded Systems 2008, 1\u201310 (2008)","journal-title":"EURASIP Journal on Embedded Systems"},{"key":"20_CR6","unstructured":"Gurevich, Y.: Logic and the Challenge of Computer Science. Current Trends in Theoretical Computer Science, pp. 1\u201357 (1988)"},{"key":"20_CR7","unstructured":"Gurevich, Y.: Evolving algebras 1993: lipari guide. In: Egon, B. (ed.) Specification and validation methods, pp. 9\u201336. Oxford University Press, Inc. (1995)"},{"key":"20_CR8","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/j.tcs.2004.11.008","volume":"336","author":"E B\u00f6rger","year":"2005","unstructured":"B\u00f6rger, E., Fruja, N.G., Gervasi, V., St\u00e4rk, R.F.: A high-level modular definition of the semantics of C#. Theoretical Computer Science 336, 235\u2013284 (2005)","journal-title":"Theoretical Computer Science"},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-1-4615-2237-9_5","volume-title":"Formal Semantics for VHDL","author":"E B\u00f6rger","year":"1995","unstructured":"B\u00f6rger, E., Gl\u00e4sser, U., Muller, W.: A formal definition of an abstract VHDL1993 simulator by EA-machines. In: Kloos, C., Breuer, P. (eds.) Formal Semantics for VHDL, pp. 107\u2013139. Springer, US (1995)"},{"key":"20_CR10","unstructured":"Gl\u00e4sser, U., Gurevich, Y., Veanes, M.: High-Level Executable Specification of the Universal Plug and Play Architecture, presented at the HICSS (2002)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"EA Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85. Springer, Heidelberg (1980)"},{"key":"20_CR12","unstructured":"Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, presented at the Logic of Programs, Workshop (1982)"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Hanisch, H.-M., Hirsch, M., Missal, D., Preu\u00dfe, S., Gerber, C.: One decade of IEC 61499 modeling and verification-results and open issues. In: 13th IFAC Symposium on Information Control Problems in Manufacturing. V.A. Trapeznikov Institute of Control Sciences, Russia (2009)","DOI":"10.3182\/20090603-3-RU-2001.0306"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Vyatkin, V., Hanisch, H.M.: Formal modeling and verification in the software engineering framework of IEC 61499: a way to self-verifying systems. In: 2001 Proceedings of 8th IEEE International Conference on Emerging Technologies and Factory Automation, vol. 2, pp. 113\u2013118 (2001)","DOI":"10.1109\/ETFA.2001.997677"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Bonfe, M., Fantuzzi, C.: Design and verification of mechatronic object-oriented models for industrial control systems. In: ETFA \u201803, IEEE Conference on Emerging Technologies and Factory Automation, vol. 2, pp. 253\u2013260 (2003)","DOI":"10.1109\/ETFA.2003.1248708"},{"key":"20_CR16","unstructured":"Dimitrova, D., Frey, G., Bachkova, I.: Formal approach for modeling and verification of IEC 61499 function blocks. In: Advanced Manufacturing Technologies (AMTECH 2005), Russe, Bulgaria, pp. 731\u2013736 (2005)"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Patil, S., Bhadra, S., Vyatkin, V.: Closed-loop formal verification framework with non-determinism, configurable by meta-modelling. In: IECON 2011 - 37th Annual Conference on IEEE Industrial Electronics Society, pp. 3770\u20133775 (2011)","DOI":"10.1109\/IECON.2011.6119923"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Vyatkin, V., Hanisch, H.M.: A modeling approach for verification of IEC1499 function blocks using net condition\/event systems. In: 1999 Proceedings of 7th IEEE International Conference on Emerging Technologies and Factory Automation. ETFA \u201899, vol. 1, pp. 261\u2013270 (1999)","DOI":"10.1109\/ETFA.1999.815365"},{"key":"20_CR19","unstructured":"Dubinin, V., Hanisch, H.M., Vyatkin, V., Shestakov, S.: Analysis of extended net condition\/event systems on the basis of model checking. presented at the Proc. Int. Conf. New Information Technologies and Systems (Originally published in Russian), Penza (2010)"},{"key":"20_CR20","unstructured":"Junbeom, Y., Sungdeok, C., Eunkyung, J.: A verification framework for FBD based software in nuclear power plants. In: Software Engineering Conference, 2008. APSEC \u201808. 15th Asia-Pacific, pp. 385\u2013392 (2008)"},{"key":"20_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/TII.2012.2186820","volume":"8","author":"VN Dubinin","year":"2012","unstructured":"Dubinin, V.N., Vyatkin, V.: Semantics-Robust Design Patterns for IEC 61499. IEEE Transactions on Industrial Informatics 8, 279\u2013290 (2012)","journal-title":"IEEE Transactions on Industrial Informatics"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Patil, S., Yan, J., Vyatkin, V., Pang, C.: On composition of mechatronic components enabled by interoperability and portability provisions of IEC 61499: A case study. In: 2013 IEEE 18th Conference on Emerging Technologies & Factory Automation (ETFA), pp. 1\u20134 (2013)","DOI":"10.1109\/ETFA.2013.6648136"},{"key":"20_CR23","unstructured":"Drozdov, D.: FB2SMV: IEC 61499 Function blocks XML code to SMV converter (2015). https:\/\/github.com\/dmitrydrozdov\/fb2smv"},{"key":"20_CR24","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-3-319-16766-4_8","volume-title":"Technological Innovation for Cloud-Based Engineering Systems","author":"S Patil","year":"2015","unstructured":"Patil, S., Drozdov, D., Dubinin, V., Vyatkin, V.: Cloud-Based Framework for Practical Model-Checking of Industrial Automation Applications. In: Camarinha-Matos, L.M., Baldissera, T.A., Di Orio, G., Marques, F. (eds.) DoCEIS 2015. IFIP AICT, vol. 450, pp. 73\u201381. Springer, Heidelberg (2015)"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Patil, S., Zahabelova, G., Vyatkin, V., McMillin, B.: Towards formal verification of smart grid distributed intelligence: FREEDM case. In: Industrial Electronics Society, IECON 2015 - 41st Annual Conference of the IEEE, Yokohama, Japan (2015)","DOI":"10.1109\/IECON.2015.7392719"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Patil, S., Vyatkin, V., McMillin, B.: Implementation of FREEDM smart grid distributed load balancing using IEC 61499 function blocks. In: Industrial Electronics Society, IECON 2013 - 39th Annual Conference of the IEEE, pp. 8154\u20138159 (2013)","DOI":"10.1109\/IECON.2013.6700497"}],"updated-by":[{"DOI":"10.1007\/978-3-319-25942-0_22","type":"erratum","label":"Erratum","source":"publisher","updated":{"date-parts":[[2016,4,5]],"date-time":"2016-04-05T00:00:00Z","timestamp":1459814400000}}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering: Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25942-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T21:50:01Z","timestamp":1748641801000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25942-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319259413","9783319259420"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25942-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"17 October 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}