{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T03:31:57Z","timestamp":1761708717711},"reference-count":35,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"6","license":[{"start":{"date-parts":[[2012,11,1]],"date-time":"2012-11-01T00:00:00Z","timestamp":1351728000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Contr. Syst. Technol."],"published-print":{"date-parts":[[2012,11]]},"DOI":"10.1109\/tcst.2011.2169262","type":"journal-article","created":{"date-parts":[[2011,11,17]],"date-time":"2011-11-17T20:47:05Z","timestamp":1321562825000},"page":"1567-1574","source":"Crossref","is-referenced-by-count":10,"title":["Towards Industrial Formal Specification of Programmable Safety Systems"],"prefix":"10.1109","volume":"20","author":[{"given":"Oscar","family":"Ljungkrantz","sequence":"first","affiliation":[]},{"given":"Knut","family":"Akesson","sequence":"additional","affiliation":[]},{"given":"Chengyin","family":"Yuan","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Fabian","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/WIFT.1998.766285"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.35"},{"key":"ref31","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/s10009-004-0175-4","article-title":"Coverage metrics for formal verification","volume":"8","author":"chockler","year":"2006","journal-title":"Int J Softw Tools for Technol Transfer"},{"key":"ref30","first-page":"39","article-title":"Verification and validation of safety applications based on PLCopen safety function blocks using timed automata in Uppaal","author":"soliman","year":"2009","journal-title":"Proc 2nd IFAC Workshop Depend Control Discrete Syst"},{"key":"ref35","author":"mcmillan","year":"1999","journal-title":"The SMV language"},{"key":"ref34","first-page":"37","article-title":"Logic controllers dependability verification using a plant model","author":"machado","year":"2006","journal-title":"Proc 3rd IFAC Workshop Discrete-Event Syst Design"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2010.2050199"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2009.67"},{"key":"ref12","first-page":"33","article-title":"Direct model checking of PLC programs in IL","author":"schlich","year":"2009","journal-title":"Proc 2nd IFAC Workshop Depend Control Discrete Syst"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2011.01.001"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04558-9"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/298595.298598"},{"key":"ref16","first-page":"176","article-title":"Safety patterns—The key to formal specification of safety requirements","volume":"2187","author":"bitsch","year":"2001","journal-title":"Proc 20th Int Conf Comput Safety Reliab Security"},{"key":"ref17","first-page":"976","article-title":"Pattern-based analysis of automated production systems","author":"campos","year":"2009","journal-title":"Proc 13th IFAC Symp Inform Control Problems Manuf"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1155\/2008\/251957"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/IDT.2008.4802520"},{"key":"ref28","first-page":"907","article-title":"Control of guarded automata counting event occurrences","author":"kozk","year":"1995","journal-title":"Proc 34th Conf Decision Control"},{"key":"ref4","author":"clarke","year":"2000","journal-title":"Model checking"},{"key":"ref27","year":"2006","journal-title":"Safety software technical specificationPart 1 Concepts and function blocks"},{"key":"ref3","year":"2010","journal-title":"Functional Safety of Electrical\/Electronic\/Programmable Electronic Safety-Related SystemsPart 3 Software Requirements"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2000.884356"},{"key":"ref29","author":"devlin","year":"2005","journal-title":"Sets Functions and LogicAn Introduction to Abstract Mathematics"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2004.1459815"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2009.2031095"},{"key":"ref7","article-title":"Improving large-sized PLC programs verification using abstractions","author":"gourcuff","year":"2008","journal-title":"17th IFAC World Congr"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/COASE.2008.4626563"},{"key":"ref9","article-title":"Counterexample-guided abstraction refinement for PLCs","author":"biallas","year":"2010","journal-title":"5th Int Workshop Syst Softw Verification"},{"key":"ref1","first-page":"32","article-title":"PLCs for safety and savings","author":"iversen","year":"2003","journal-title":"Autom World"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2009.5195876"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1016\/S1071-5819(03)00115-0"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2010.5549591"},{"key":"ref24","first-page":"17","author":"ljungkrantz","year":"2010","journal-title":"Programmable Logic Controller"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1108\/01445150810849000"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1049\/PBCE050E"},{"key":"ref25","first-page":"21","article-title":"Lightweight formal methods","author":"jackson","year":"1996","journal-title":"IEEE Comput"}],"container-title":["IEEE Transactions on Control Systems Technology"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/87\/6264111\/06081966.pdf?arnumber=6081966","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,10]],"date-time":"2021-10-10T23:47:18Z","timestamp":1633909638000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6081966\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11]]},"references-count":35,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.1109\/tcst.2011.2169262","relation":{},"ISSN":["1063-6536","1558-0865"],"issn-type":[{"value":"1063-6536","type":"print"},{"value":"1558-0865","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,11]]}}}