{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T08:09:27Z","timestamp":1777450167307,"version":"3.51.4"},"reference-count":18,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,5]]},"DOI":"10.1109\/eit.2016.7535242","type":"proceedings-article","created":{"date-parts":[[2016,8,15]],"date-time":"2016-08-15T18:39:48Z","timestamp":1471286388000},"page":"0211-0216","source":"Crossref","is-referenced-by-count":16,"title":["Model-based verification of PLC programs using Simulink design"],"prefix":"10.1109","author":[{"given":"Nannan","family":"He","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor","family":"Oke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gale","family":"Allen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"ref11","first-page":"228","article-title":"Trasnformation from Petri Nets model to programmable logic controller using one-to-one mapping technique","volume":"2","author":"thapa","year":"2005","journal-title":"Proceedings of Intl conf on Computational Intelligence for Modeling Control and Automation"},{"key":"ref12","first-page":"796","article-title":"Obtaining formal models from Ladder diagrams","author":"oliveira","year":"2011","journal-title":"Proc IEEE Int Conf Ind Informatics"},{"key":"ref13","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 Intl Conf on Automation of Mixed Processes"},{"key":"ref14","first-page":"184","article-title":"Detecting races in relay ladder logic programs","author":"kiken","year":"1998","journal-title":"Lecture Notes in Computer Science 1394"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.3182\/20080706-5-KR-1001.01786"},{"key":"ref16","first-page":"905","article-title":"Safety properties verification of ladder diagram programs","volume":"36","author":"roussel","year":"2002","journal-title":"J Eur Syst Automat"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69100-6_9"},{"key":"ref18","article-title":"Experiences with the Gene-Auto Code Generator in the Aerospace Industry","author":"rugina","year":"2010","journal-title":"Proceedings of Intl Conf on Embedded Real-Time Software and Systems ERTS 2"},{"key":"ref4","year":"0"},{"key":"ref3","first-page":"9","article-title":"Towards Automatic Verification of Ladder Logic Programs","author":"zoubek","year":"2003","journal-title":"Proc IMACS-IEEE CESA"},{"key":"ref6","author":"clarke","year":"1999","journal-title":"Model Checking (MIT Press"},{"key":"ref5","first-page":"1107","article-title":"Interpretation Petri net model to IEC 1131–3: LD for programmable logic controller","author":"suesut","year":"2004","journal-title":"Proc IEEE Conf on Robotics Automat Mechatronics"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2000.884356"},{"key":"ref7","first-page":"168","article-title":"A tool for checking ANSI-C programs","author":"clarke","year":"2004","journal-title":"proceedings of TACAS"},{"key":"ref2","year":"0"},{"key":"ref1","year":"0"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.compind.2010.05.015"}],"event":{"name":"2016 IEEE International Conference on Electro Information Technology (EIT)","location":"Grand Forks, ND, USA","start":{"date-parts":[[2016,5,19]]},"end":{"date-parts":[[2016,5,21]]}},"container-title":["2016 IEEE International Conference on Electro Information Technology (EIT)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7527136\/7535221\/07535242.pdf?arnumber=7535242","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2016,9,29]],"date-time":"2016-09-29T19:03:12Z","timestamp":1475175792000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7535242\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5]]},"references-count":18,"URL":"https:\/\/doi.org\/10.1109\/eit.2016.7535242","relation":{},"subject":[],"published":{"date-parts":[[2016,5]]}}}