{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T14:37:37Z","timestamp":1773758257467,"version":"3.50.1"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T00:00:00Z","timestamp":1754352000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T00:00:00Z","timestamp":1754352000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100020950","name":"National Science and Technology Council","doi-asserted-by":"publisher","award":["NSTC 113-2221-E-006-128-"],"award-info":[{"award-number":["NSTC 113-2221-E-006-128-"]}],"id":[{"id":"10.13039\/501100020950","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2026,4]]},"DOI":"10.1007\/s10270-025-01316-y","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:57:59Z","timestamp":1754369879000},"page":"615-633","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automatic Model Transformation and Formal Verification for Function Block of IEC 61499"],"prefix":"10.1007","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4841-4838","authenticated-orcid":false,"given":"Yean-Ru","family":"Chen","sequence":"first","affiliation":[]},{"given":"Chia-Hao","family":"Hsu","sequence":"additional","affiliation":[]},{"given":"Tien-Fu","family":"Li","sequence":"additional","affiliation":[]},{"given":"Cheng-Yuan","family":"Lin","sequence":"additional","affiliation":[]},{"given":"Shao-Chia","family":"Weng","sequence":"additional","affiliation":[]},{"given":"Min-Yan","family":"Tsai","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"1316_CR1","doi-asserted-by":"crossref","unstructured":"Nakahori, K., Yamaguchi, S.: A support tool to design iot services with nusmv. In: 2017 IEEE International Conference on Consumer Electronics (ICCE), pp. 80\u201383 (2017). IEEE","DOI":"10.1109\/ICCE.2017.7889238"},{"key":"1316_CR2","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 7th IEEE International Conference on Emerging Technologies and Factory Automation. Proceedings ETFA\u201999 (Cat. No. 99TH8467), (1), 261\u2013270 (1999). IEEE","DOI":"10.1109\/ETFA.1999.815365"},{"key":"1316_CR3","doi-asserted-by":"crossref","unstructured":"Schnakenbourg, C., Faure, J.-M., Lesage, J.-J.: Towards iec 61499 function blocks diagrams verification. In: IEEE International Conference on Systems, Man and Cybernetics, (3), 6 (2002). IEEE","DOI":"10.1109\/ICSMC.2002.1176038"},{"issue":"1","key":"1316_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/LES.2010.2042275","volume":"2","author":"LH Yoong","year":"2010","unstructured":"Yoong, L.H., Roop, P.S.: Verifying iec 61499 function blocks using esterel. IEEE Embed. Syst. Lett. 2(1), 1\u20134 (2010)","journal-title":"IEEE Embed. Syst. Lett."},{"key":"1316_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem. In: LASER Summer School on Software Engineering, 1\u201330 (2011). Springer","DOI":"10.1007\/978-3-642-35746-6_1"},{"key":"1316_CR6","doi-asserted-by":"crossref","unstructured":"Brim, L., \u010ce\u0161ka, M., \u0160afr\u00e1nek, D.: Model checking of biological systems. In: International School on Formal Methods for the Design of Computer, Communication and Software Systems, 63\u2013112 (2013). Springer","DOI":"10.1007\/978-3-642-38874-3_3"},{"key":"1316_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, 19\u201329 (2002). IEEE","DOI":"10.1109\/LICS.2002.1029814"},{"key":"1316_CR8","doi-asserted-by":"crossref","unstructured":"Patil, S., Vyatkin, V., Pang, C.: Counterexample-guided simulation framework for formal verification of flexible automation systems. In: 2015 IEEE 13th International Conference on Industrial Informatics (INDIN), 1192\u20131197 (2015). IEEE","DOI":"10.1109\/INDIN.2015.7281905"},{"key":"1316_CR9","unstructured":"Christensen, J.H., Strasser, T., Valentini, A., Vyatkin, V., Zoitl, A.: The iec 61499 function block standard: Overview of the second edition. ISA autom. Week 6, 6\u20137 (2012)"},{"key":"1316_CR10","doi-asserted-by":"crossref","unstructured":"Lin, S.-W., Liu, Y., Hsiung, P.-A., Sun, J., Dong, J.S.: Automatic generation of provably correct embedded systems. In: International Conference on Formal Engineering Methods, pp. 214\u2013229 (2012). Springer","DOI":"10.1007\/978-3-642-34281-3_17"},{"issue":"1","key":"1316_CR11","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1145\/1925844.1926446","volume":"46","author":"Y Feng","year":"2011","unstructured":"Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. Acm Sigplan Notices 46(1), 523\u2013534 (2011)","journal-title":"Acm Sigplan Notices"},{"key":"1316_CR12","unstructured":"Moore, R., Lopes, J.: Paper templates. In: TEMPLATE\u201906, 1st International Conference on Template Production, 319\u2013340 (1999)"},{"key":"1316_CR13","doi-asserted-by":"crossref","unstructured":"Dubinin, V., Vyatkin, V., Shalyto, A.: Formal modeling and verification of iec 61499 function blocks on the basis of transition systems. In: 2016 International Siberian Conference on Control and Communications (SIBCON), 1\u20134 (2016). IEEE","DOI":"10.1109\/SIBCON.2016.7491701"},{"key":"1316_CR14","unstructured":"Commission, I., et al.: International standard iec61499-1. Function Blocks-Part 1 Architecture (2005)"},{"key":"1316_CR15","doi-asserted-by":"crossref","unstructured":"Yan, J., Vyatkin, V.V.: Distributed execution and cyber-physical design of baggage handling automation with iec 61499. In: 2011 9th IEEE International Conference on Industrial Informatics, 573\u2013578 (2011). IEEE","DOI":"10.1109\/INDIN.2011.6034942"},{"key":"1316_CR16","doi-asserted-by":"crossref","unstructured":"Colla, M., Brusaferri, A., Carpanzano, E.: Applying the iec-61499 model to the shoe manufacturing sector. In: 2006 IEEE Conference on Emerging Technologies and Factory Automation, 1301\u20131308 (2006). IEEE","DOI":"10.1109\/ETFA.2006.355422"},{"key":"1316_CR17","doi-asserted-by":"crossref","unstructured":"Sorouri, M., Patil, S., Salcic, Z., Vyatkin, V.: Software composition and distributed operation scheduling in modular automated machines. IEEE Trans. Industr. Inf. 11(4), 865\u2013878 (2015)","DOI":"10.1109\/TII.2015.2430836"},{"key":"1316_CR18","doi-asserted-by":"crossref","unstructured":"Pang, C., Vyatkin, V., Deng, Y., Sorouri, M.: Virtual smart metering in automation and simulation of energy-efficient lighting system. In: 2013 IEEE 18th Conference on Emerging Technologies & Factory Automation (ETFA), 1\u20138 (2013). IEEE","DOI":"10.1109\/ETFA.2013.6648040"},{"key":"1316_CR19","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: IECON 2013-39th Annual Conference of the IEEE Industrial Electronics Society, 8154\u20138159 (2013). IEEE","DOI":"10.1109\/IECON.2013.6700497"},{"key":"1316_CR20","doi-asserted-by":"crossref","unstructured":"Zhabelova, G., Patil, S., Yang, C.-w., Vyatkin, V.: Smart grid applications with iec 61499 reference architecture. In: 2013 11th Ieee International Conference on Industrial Informatics (indin), 458\u2013463 (2013). IEEE","DOI":"10.1109\/INDIN.2013.6622928"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-025-01316-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-025-01316-y","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-025-01316-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T12:01:56Z","timestamp":1773748916000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-025-01316-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,4]]}},"alternative-id":["1316"],"URL":"https:\/\/doi.org\/10.1007\/s10270-025-01316-y","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"16 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 April 2025","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 June 2025","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 August 2025","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}