{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:51:42Z","timestamp":1750308702620,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"\u03b5CEDAC project","award":["FFG 809447"],"award-info":[{"award-number":["FFG 809447"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2013,1]]},"abstract":"<jats:p>This article presents a new formal approach to validation of on-the-fly modification of control software in automation systems. The concept of downtimeless system evolution (DSE) is introduced. The DSE is essentially based on the use of IEC 61499 system architecture and formal modeling and verification of the hardware and software of an automation device. The validation is performed by means of two complimentary techniques: analytic calculations and formal verification by model-checking.<\/jats:p>","DOI":"10.1145\/2406336.2406353","type":"journal-article","created":{"date-parts":[[2013,1,29]],"date-time":"2013-01-29T16:20:55Z","timestamp":1359476455000},"page":"1-17","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Formal Verification of Downtimeless System Evolution in Embedded Automation Controllers"],"prefix":"10.1145","volume":"12","author":[{"given":"Christoph","family":"S\u00fcnder","sequence":"first","affiliation":[{"name":"Thales GmbH, Austria"}]},{"given":"Valeriy","family":"Vyatkin","sequence":"additional","affiliation":[{"name":"The University of Auckland, New Zealand"}]},{"given":"Alois","family":"Zoitl","sequence":"additional","affiliation":[{"name":"Technical University of Vienna, Austria"}]}],"member":"320","published-online":{"date-parts":[[2013,1]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"4DIAC IDE. 2010. http:\/\/www.fordiac.org\/.  4DIAC IDE. 2010. http:\/\/www.fordiac.org\/."},{"key":"e_1_2_1_2_1","volume-title":"Petri Net Model Reconfiguration of Discrete Manufacturing Systems. In Proceedings of the 12th IFAC Symposium on Information Control Problems in Manufacturing","volume":"1","author":"Alcaraz-Mej\u00eda M.","unstructured":"Alcaraz-Mej\u00eda , M. and L\u00f3pez-Mellado , E . 2006 . Petri Net Model Reconfiguration of Discrete Manufacturing Systems. In Proceedings of the 12th IFAC Symposium on Information Control Problems in Manufacturing , vol. 1 , 547--552. Alcaraz-Mej\u00eda, M. and L\u00f3pez-Mellado, E. 2006. Petri Net Model Reconfiguration of Discrete Manufacturing Systems. In Proceedings of the 12th IFAC Symposium on Information Control Problems in Manufacturing, vol. 1, 547--552."},{"volume-title":"Proceedings of IEEE International Conference on Industrial Informatics (INDIN\u201907)","author":"Baier T.","key":"e_1_2_1_3_1","unstructured":"Baier , T. , Fritsche , J. , Keintzel , G. , Loy , D. , Schranz , R. , Steininger , H. , Strasser , T. , and S\u00fcnder , C . 2007. Future scenarios for application of downtimeless reconfiguration in industrial practice . In Proceedings of IEEE International Conference on Industrial Informatics (INDIN\u201907) . 1129--1134. Baier, T., Fritsche, J., Keintzel, G., Loy, D., Schranz, R., Steininger, H., Strasser, T., and S\u00fcnder, C. 2007. Future scenarios for application of downtimeless reconfiguration in industrial practice. In Proceedings of IEEE International Conference on Industrial Informatics (INDIN\u201907). 1129--1134."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1275687.1275693"},{"key":"e_1_2_1_5_1","article-title":"Transition Management for Reconfigurable Hybrid Control Systems","volume":"23","author":"Guler M.","year":"2003","unstructured":"Guler , M. , Clements , S. , Wills , L. M. , Heck , B. S. , and Vachtsevanos , G. J. 2003 , Transition Management for Reconfigurable Hybrid Control Systems . IEEE Control Systems Magazine 23 , 1, 2003, 36--49. Guler, M., Clements, S., Wills, L. M., Heck, B. S., and Vachtsevanos, G. J. 2003, Transition Management for Reconfigurable Hybrid Control Systems. IEEE Control Systems Magazine 23, 1, 2003, 36--49.","journal-title":"IEEE Control Systems Magazine"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1504\/IJMTM.2006.008802"},{"key":"e_1_2_1_7_1","unstructured":"ICS TRIPLEX. 2011. ISaGRAF Workbench for IEC 61499\/ 61131 v.5.1 http:\/\/www.icstriplex.com\/.  ICS TRIPLEX. 2011. ISaGRAF Workbench for IEC 61499\/ 61131 v.5.1 http:\/\/www.icstriplex.com\/."},{"key":"e_1_2_1_8_1","volume-title":"Int. Standard. International Electrotechnical Commission (IEC)","author":"Function","year":"2005","unstructured":"IEC 61499-1 Function blocks---Part 1 : Architecture , Int. Standard. International Electrotechnical Commission (IEC) , 2005 . IEC 61499-1 Function blocks---Part 1: Architecture, Int. Standard. International Electrotechnical Commission (IEC), 2005."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRA.2002.802206"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/19.948303"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.232231"},{"key":"e_1_2_1_12_1","first-page":"6","article-title":"Software evolution in the age of component-based software engineering","volume":"147","author":"Lehmann M.","year":"2000","unstructured":"Lehmann , M. and Ramil , J. 2000 . Software evolution in the age of component-based software engineering . IEEE Proc. Softw. 147 , 6 . Lehmann, M. and Ramil, J. 2000. Software evolution in the age of component-based software engineering. IEEE Proc. Softw. 147, 6.","journal-title":"IEEE Proc. Softw."},{"volume-title":"Proceedings of the IEEE International Conference on Mechatronics and Automation. 592--567","author":"Li J.","key":"e_1_2_1_13_1","unstructured":"Li , J. , Dai , X. , and Meng , Z . 2005. Dynamic reconfiguration of Petri net logic controllers based on modified net rewriting systems . In Proceedings of the IEEE International Conference on Mechatronics and Automation. 592--567 . Li, J., Dai, X., and Meng, Z. 2005. Dynamic reconfiguration of Petri net logic controllers based on modified net rewriting systems. In Proceedings of the IEEE International Conference on Mechatronics and Automation. 592--567."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/IWPSE.2005.7"},{"key":"e_1_2_1_15_1","unstructured":"NxtControl GMBH. 2011. nxtControl - Next generation software for next generation customers. http:\/\/www.nxtcontrol.com\/.  NxtControl GMBH. 2011. nxtControl - Next generation software for next generation customers. http:\/\/www.nxtcontrol.com\/."},{"volume-title":"Proceedings of the 5th IEEE International Conference on Industrial Informatics (INDIN\u201907)","author":"Pang C.","key":"e_1_2_1_16_1","unstructured":"Pang , C. and Vyatkin , V . 2007. Formal modelling of IEC61499 systems following the Sequential Hypothesis . In Proceedings of the 5th IEEE International Conference on Industrial Informatics (INDIN\u201907) . 879--884. Pang, C. and Vyatkin, V. 2007. Formal modelling of IEC61499 systems following the Sequential Hypothesis. In Proceedings of the 5th IEEE International Conference on Industrial Informatics (INDIN\u201907). 879--884."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/5326.941841"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the INRA\/IEEE Symposium on Emerging Technologies and Factory Automation","volume":"1","author":"Rausch M.","unstructured":"Rausch , M. and Hanisch , H . -M. 1995. Net condition\/event systems with multiple condition outputs . In Proceedings of the INRA\/IEEE Symposium on Emerging Technologies and Factory Automation , vol. 1 . 592--600. Rausch, M. and Hanisch, H.-M. 1995. Net condition\/event systems with multiple condition outputs. In Proceedings of the INRA\/IEEE Symposium on Emerging Technologies and Factory Automation, vol. 1. 592--600."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74481-8_31"},{"key":"e_1_2_1_21_1","article-title":"Functional and temporal formal modeling of embedded controllers for intelligent mechatronic systems","volume":"2","author":"S\u00fcnder C.","year":"2009","unstructured":"S\u00fcnder , C. and Vyatkin , V. 2009 . Functional and temporal formal modeling of embedded controllers for intelligent mechatronic systems . Intl. J. Mechatronics Manuf. Syst. 2 , 1\/2, 215--235. S\u00fcnder, C. and Vyatkin, V. 2009. Functional and temporal formal modeling of embedded controllers for intelligent mechatronic systems. Intl. J. Mechatronics Manuf. Syst. 2, 1\/2, 215--235.","journal-title":"Intl. J. Mechatronics Manuf. Syst."},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Te\u0161anovi\u0107 A. Nadjm-Tehrani S. and \n      Hansson J\n  . \n  2005\n  . Modular Verification of reconfigurable components. In Component-Based Software Development for Embedded Systems Lecture Notes in Computer Science vol. \n  3778 C. Atkinson et al. Eds. \n  Springer 59--81.  Te\u0161anovi\u0107 A. Nadjm-Tehrani S. and Hansson J. 2005. Modular Verification of reconfigurable components. In Component-Based Software Development for Embedded Systems Lecture Notes in Computer Science vol. 3778 C. Atkinson et al. Eds. Springer 59--81.","DOI":"10.1007\/11591962_4"},{"volume-title":"IEC 61499 Function Blocks for Embedded and Distributed Control Systems Design, 297","author":"Vyatkin V.","key":"e_1_2_1_23_1","unstructured":"Vyatkin , V. 2007. IEC 61499 Function Blocks for Embedded and Distributed Control Systems Design, 297 . Instrumentation Society of America . Vyatkin, V. 2007. IEC 61499 Function Blocks for Embedded and Distributed Control Systems Design, 297. Instrumentation Society of America."},{"key":"e_1_2_1_24_1","unstructured":"Vyatkin V. 2009. Visual Verification Framework Version 0.35a http:\/\/www.ece.auckland.ac.nz\/~vyatkin\/vive\/ViVe.zip.  Vyatkin V. 2009. Visual Verification Framework Version 0.35a http:\/\/www.ece.auckland.ac.nz\/~vyatkin\/vive\/ViVe.zip."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1155\/2008\/251957"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022295414523"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-006-0038-4"},{"key":"e_1_2_1_28_1","unstructured":"Zoitl A. 2009. Real-Time Execution for IEC 61499 ISA.   Zoitl A. 2009. Real-Time Execution for IEC 61499 ISA."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2406336.2406353","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2406336.2406353","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:13:55Z","timestamp":1750277635000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2406336.2406353"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["10.1145\/2406336.2406353"],"URL":"https:\/\/doi.org\/10.1145\/2406336.2406353","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2013,1]]},"assertion":[{"value":"2010-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}