{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T14:36:05Z","timestamp":1773326165519,"version":"3.50.1"},"reference-count":4,"publisher":"Wiley","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"funder":[{"name":"International S&T Cooperation Program of China","award":["2011DFG13000"],"award-info":[{"award-number":["2011DFG13000"]}]},{"name":"International S&T Cooperation Program of China","award":["2010DFB10930"],"award-info":[{"award-number":["2010DFB10930"]}]},{"name":"International S&T Cooperation Program of China","award":["4122017"],"award-info":[{"award-number":["4122017"]}]},{"name":"International S&T Cooperation Program of China","award":["KZ201210028036"],"award-info":[{"award-number":["KZ201210028036"]}]},{"name":"Mechanism and Verification of High-speed Embedded Communication Systems in Rugged Environment","award":["2011DFG13000"],"award-info":[{"award-number":["2011DFG13000"]}]},{"name":"Mechanism and Verification of High-speed Embedded Communication Systems in Rugged Environment","award":["2010DFB10930"],"award-info":[{"award-number":["2010DFB10930"]}]},{"name":"Mechanism and Verification of High-speed Embedded Communication Systems in Rugged Environment","award":["4122017"],"award-info":[{"award-number":["4122017"]}]},{"name":"Mechanism and Verification of High-speed Embedded Communication Systems in Rugged Environment","award":["KZ201210028036"],"award-info":[{"award-number":["KZ201210028036"]}]},{"DOI":"10.13039\/501100004826","name":"Natural Science Foundation of Beijing Municipality","doi-asserted-by":"publisher","award":["2011DFG13000"],"award-info":[{"award-number":["2011DFG13000"]}],"id":[{"id":"10.13039\/501100004826","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004826","name":"Natural Science Foundation of Beijing Municipality","doi-asserted-by":"publisher","award":["2010DFB10930"],"award-info":[{"award-number":["2010DFB10930"]}],"id":[{"id":"10.13039\/501100004826","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004826","name":"Natural Science Foundation of Beijing Municipality","doi-asserted-by":"publisher","award":["4122017"],"award-info":[{"award-number":["4122017"]}],"id":[{"id":"10.13039\/501100004826","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004826","name":"Natural Science Foundation of Beijing Municipality","doi-asserted-by":"publisher","award":["KZ201210028036"],"award-info":[{"award-number":["KZ201210028036"]}],"id":[{"id":"10.13039\/501100004826","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002888","name":"Beijing Municipal Commission of Education","doi-asserted-by":"publisher","award":["2011DFG13000"],"award-info":[{"award-number":["2011DFG13000"]}],"id":[{"id":"10.13039\/501100002888","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002888","name":"Beijing Municipal Commission of Education","doi-asserted-by":"publisher","award":["2010DFB10930"],"award-info":[{"award-number":["2010DFB10930"]}],"id":[{"id":"10.13039\/501100002888","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002888","name":"Beijing Municipal Commission of Education","doi-asserted-by":"publisher","award":["4122017"],"award-info":[{"award-number":["4122017"]}],"id":[{"id":"10.13039\/501100002888","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002888","name":"Beijing Municipal Commission of Education","doi-asserted-by":"publisher","award":["KZ201210028036"],"award-info":[{"award-number":["KZ201210028036"]}],"id":[{"id":"10.13039\/501100002888","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002888","name":"Beijing Municipal Commission of Education","doi-asserted-by":"publisher","award":["2011DFG13000"],"award-info":[{"award-number":["2011DFG13000"]}],"id":[{"id":"10.13039\/501100002888","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002888","name":"Beijing Municipal Commission of Education","doi-asserted-by":"publisher","award":["2010DFB10930"],"award-info":[{"award-number":["2010DFB10930"]}],"id":[{"id":"10.13039\/501100002888","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002888","name":"Beijing Municipal Commission of Education","doi-asserted-by":"publisher","award":["4122017"],"award-info":[{"award-number":["4122017"]}],"id":[{"id":"10.13039\/501100002888","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002888","name":"Beijing Municipal Commission of Education","doi-asserted-by":"publisher","award":["KZ201210028036"],"award-info":[{"award-number":["KZ201210028036"]}],"id":[{"id":"10.13039\/501100002888","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Mathematics"],"published-print":{"date-parts":[[2013]]},"abstract":"<jats:p>Functional validation is an important task in complex embedded system. The formal modeling of PLC system for verification is a rough task. Good verification model should be faithful and concise. At one hand, the model must be consistent with the system at the other hand, the model must have suitable scale because of the state explosion problem of verification. This paper proposes a systemic method for the construction of verification model. PLC system architecture and PLC features are modeled as components. This is universal for all PLC applications. We give an automatic translation method for software modeling based on operational semantics. A small example is demonstrated for our approach.<\/jats:p>","DOI":"10.1155\/2013\/721624","type":"journal-article","created":{"date-parts":[[2013,4,22]],"date-time":"2013-04-22T23:03:45Z","timestamp":1366671825000},"page":"1-9","source":"Crossref","is-referenced-by-count":7,"title":["Component-Based Formal Modeling of PLC Systems"],"prefix":"10.1155","volume":"2013","author":[{"given":"Rui","family":"Wang","sequence":"first","affiliation":[{"name":"College of Information Engineering, Capital Normal University, Beijing 100048, China"},{"name":"National Lab for ISAT, Beijing 100048, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[{"name":"College of Information Engineering, Capital Normal University, Beijing 100048, China"},{"name":"National Lab for ISAT, Beijing 100048, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luo","family":"Liming","sequence":"additional","affiliation":[{"name":"College of Information Engineering, Capital Normal University, Beijing 100048, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaojuan","family":"Li","sequence":"additional","affiliation":[{"name":"College of Information Engineering, Capital Normal University, Beijing 100048, China"},{"name":"National Lab for ISAT, Beijing 100048, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie","family":"Zhang","sequence":"additional","affiliation":[{"name":"College of Information Science and Technology, Beijing University of Chemical Technology, Beijing 100029, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","reference":[{"key":"1","year":"1999"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.09.026"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2011.27"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2010.2069102"}],"container-title":["Journal of Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/721624.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/721624.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/721624.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2016,9,28]],"date-time":"2016-09-28T17:08:52Z","timestamp":1475082532000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.hindawi.com\/journals\/jam\/2013\/721624\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"references-count":4,"alternative-id":["721624","721624"],"URL":"https:\/\/doi.org\/10.1155\/2013\/721624","relation":{},"ISSN":["1110-757X","1687-0042"],"issn-type":[{"value":"1110-757X","type":"print"},{"value":"1687-0042","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}