{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T23:07:25Z","timestamp":1760828845543},"reference-count":30,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009,9]]},"DOI":"10.1109\/etfa.2009.5347044","type":"proceedings-article","created":{"date-parts":[[2009,12,10]],"date-time":"2009-12-10T14:44:11Z","timestamp":1260456251000},"page":"1-7","source":"Crossref","is-referenced-by-count":14,"title":["Formal verification of UML-modeled machine controls"],"prefix":"10.1109","author":[{"given":"Thomas","family":"Klotz","sequence":"first","affiliation":[{"name":"Fraunhofer Institute for Integrated Circuits, Design Automation Division, Zeunerstr. 38, 01069 Dresden, Germany"}]},{"given":"Eva","family":"Fordran","sequence":"additional","affiliation":[{"name":"Fraunhofer Institute for Integrated Circuits, Design Automation Division, Zeunerstr. 38, 01069 Dresden, Germany"}]},{"given":"Bernd","family":"Straube","sequence":"additional","affiliation":[{"name":"Fraunhofer Institute for Integrated Circuits, Design Automation Division, Zeunerstr. 38, 01069 Dresden, Germany"}]},{"given":"Jurgen","family":"Haufe","sequence":"additional","affiliation":[{"name":"Fraunhofer Institute for Integrated Circuits, Design Automation Division, Zeunerstr. 38, 01069 Dresden, Germany"}]}],"member":"263","reference":[{"key":"ref30","article-title":"Towards automatic verification of ladder logic programs","author":"zoubek","year":"2003","journal-title":"CESA '03 Proceedings of the IMACS Multiconference on Computational Engineering in Systems Applications"},{"key":"ref10","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0055332","article-title":"On the Need for Practical Formal Methods","author":"heitmeyer","year":"1998","journal-title":"Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems FTRTFT '98"},{"journal-title":"International Electrotechnical Commission IEC Standard 61131-3 Programmable controllers - Part 3","year":"1993","key":"ref11"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2006.07.005"},{"journal-title":"J+P Maschinenbau GmbH Case filling Machine KV 250\/400 datasheet","article-title":"accessed","year":"2009","key":"ref13"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2009.5347044"},{"article-title":"Model Driven Development of Certifiable Software: A Best Practice for Safety-Critical Applications. Embedded Market Forecasters","year":"2008","author":"krasner","key":"ref15"},{"key":"ref16","article-title":"Rapid Control Prototyping by Transformation of Hierachical State Machine Control Models into IEC 61131 PLC Code","author":"lindner","year":"2009","journal-title":"diploma thesis"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2005.1612527"},{"article-title":"Symbolic Model Checking","year":"1993","author":"mcmillan","key":"ref18"},{"year":"2007","key":"ref19","article-title":"Modelica Association. Modelica Language Specification Version 3.0"},{"article-title":"Programmable Logic Controllers: Principles and Applications","year":"2002","author":"webb","key":"ref28"},{"journal-title":"Model checking","year":"2000","author":"clarke","key":"ref4"},{"journal-title":"Uppaal model checker web page","article-title":"Uppaal Developer Team","year":"2009","key":"ref27"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","article-title":"NuSMV 2: An OpenSource Tool for Symbolic Model Checking","author":"cimatti","year":"2002","journal-title":"CAV '02 Proceedings of the 14th International Conference on Computer Aided Verification"},{"year":"2009","key":"ref6","article-title":"Esterel Technologies. Esterel Studio web page"},{"key":"ref29","first-page":"613","article-title":"Formalization of PLC Programs to Sustain Reliability","author":"younis","year":"2004","journal-title":"Proceedings of the 2004 IEEE Conference on Robotics Automation and Mechatronics"},{"key":"ref5","first-page":"269","article-title":"A new Approach for Modeling and Verification of Discrete Control Components within a Modelica Environment","author":"donath","year":"2008","journal-title":"Proceedings of the 6th International Modelica Conference"},{"key":"ref8","article-title":"Statecharts: A Visual Approach to Complex Systems","author":"harel","year":"1984","journal-title":"Technical Report CS84-05"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2006.1678428"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01257083"},{"key":"ref9","first-page":"367","article-title":"Simulation-supported Prototyping and Optimsation of Machine Controls","author":"haufe","year":"2008","journal-title":"Advances in Simulation for Production and Logistics Applications"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/37.272781"},{"journal-title":"XMI Specification version 2 1 1","article-title":"Object Management Group","year":"2007","key":"ref22"},{"journal-title":"Unified Modeling Language Specification Version 1 5","article-title":"Object Management Group","year":"2007","key":"ref21"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"ref23","article-title":"Automation of Formal Verification of PLC Programs Written in IL","author":"pavlovic","year":"2007","journal-title":"VERIFY '07 Proceedings of the 4th International Verification Workshop"},{"journal-title":"Products Web Page","article-title":"The Mathworks","year":"2009","key":"ref26"},{"key":"ref25","first-page":"177","article-title":"Formal Modeling of Timed Function Blocks for the Automatic Verification of Ladder Diagram Programs","author":"rossi","year":"2000","journal-title":"Proceedings of the 4th International Conference on Automation of Mixed Processes"}],"event":{"name":"2009 IEEE Conference on Emerging Technologies & Factory Automation (ETFA 2009)","start":{"date-parts":[[2009,9,22]]},"location":"Palma de Mallorca, Spain","end":{"date-parts":[[2009,9,25]]}},"container-title":["2009 IEEE Conference on Emerging Technologies & Factory Automation"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5340902\/5346987\/05347044.pdf?arnumber=5347044","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,8]],"date-time":"2021-06-08T10:57:18Z","timestamp":1623149838000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/5347044\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,9]]},"references-count":30,"URL":"https:\/\/doi.org\/10.1109\/etfa.2009.5347044","relation":{},"subject":[],"published":{"date-parts":[[2009,9]]}}}