{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:03:20Z","timestamp":1768003400401,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,3,13]],"date-time":"2018-03-13T00:00:00Z","timestamp":1520899200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,3,13]]},"DOI":"10.1145\/3176258.3176949","type":"proceedings-article","created":{"date-parts":[[2018,3,15]],"date-time":"2018-03-15T13:22:14Z","timestamp":1521120134000},"page":"164-166","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Model Checking of Security Properties in Industrial Control Systems (ICS)"],"prefix":"10.1145","author":[{"given":"Roshan","family":"Shrestha","sequence":"first","affiliation":[{"name":"Boise State University, Boise, ID, USA"}]},{"given":"Hoda","family":"Mehrpouyan","sequence":"additional","affiliation":[{"name":"Boise State University, Boise, ID, USA"}]},{"given":"Dianxiang","family":"Xu","sequence":"additional","affiliation":[{"name":"Boise State University, Boise, ID, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,3,13]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Experion PKS Orion - Process Control Beyond Distributed Control Systems. https:\/\/www.honeywellprocess.com\/ en-US\/explore\/products\/control-monitoring-and-safety-systems\/ integrated-control-and-safety-systems\/experion-pks\/Pages\/experionpks.aspx.  Experion PKS Orion - Process Control Beyond Distributed Control Systems. https:\/\/www.honeywellprocess.com\/ en-US\/explore\/products\/control-monitoring-and-safety-systems\/ integrated-control-and-safety-systems\/experion-pks\/Pages\/experionpks.aspx."},{"key":"e_1_3_2_1_2_1","unstructured":"Honeywell C300 controller. https:\/\/www.honeywellprocess.com\/ en-US\/explore\/products\/control-monitoring-and-safety-systems\/integrated-control-and-safety-systems\/experion-pks\/controllers\/Pages\/ c300.aspx.  Honeywell C300 controller. https:\/\/www.honeywellprocess.com\/ en-US\/explore\/products\/control-monitoring-and-safety-systems\/integrated-control-and-safety-systems\/experion-pks\/controllers\/Pages\/ c300.aspx."},{"key":"e_1_3_2_1_3_1","volume-title":"Principles of model checking","author":"Baier Christel","unstructured":"Christel Baier , Joost-Pieter Katoen , and Kim Guldstrand Larsen . 2008. Principles of model checking . MIT press . Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen. 2008. Principles of model checking. MIT press."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijcip.2013.04.004"},{"key":"e_1_3_2_1_5_1","volume-title":"Systems and software verification: model-checking techniques and tools","author":"B\u00e9rard B\u00e9atrice","unstructured":"B\u00e9atrice B\u00e9rard , Michel Bidoit , Alain Finkel , Fran\u00e7ois Laroussinie , Antoine Petit , Laure Petrucci , and Philippe Schnoebelen . 2013. Systems and software verification: model-checking techniques and tools . Springer Science & Business Media . B\u00e9atrice B\u00e9rard, Michel Bidoit, Alain Finkel, Fran\u00e7ois Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. 2013. Systems and software verification: model-checking techniques and tools. Springer Science & Business Media."},{"key":"e_1_3_2_1_6_1","volume-title":"Symbolic model checking without BDDs. Tools and Algorithms for the Construction and Analysis of Systems","author":"Biere Armin","year":"1999","unstructured":"Armin Biere , Alessandro Cimatti , Edmund Clarke , and Yunshan Zhu . 1999. Symbolic model checking without BDDs. Tools and Algorithms for the Construction and Analysis of Systems ( 1999 ), 193--207. Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. 1999. Symbolic model checking without BDDs. Tools and Algorithms for the Construction and Analysis of Systems (1999), 193--207."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"William Bolton. 2015. Programmable logic controllers. Newnes.   William Bolton. 2015. Programmable logic controllers. Newnes.","DOI":"10.1016\/B978-0-12-802929-9.00001-7"},{"key":"e_1_3_2_1_8_1","volume-title":"SCADA: supervisory control and data acquisition","author":"Boyer Stuart A","unstructured":"Stuart A Boyer . 2009. SCADA: supervisory control and data acquisition . International Society of Automation . Stuart A Boyer. 2009. SCADA: supervisory control and data acquisition. International Society of Automation."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734431"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/647768.733923"},{"key":"e_1_3_2_1_11_1","volume-title":"What is SCADA?","author":"Daneels Axel","year":"1999","unstructured":"Axel Daneels and Wayne Salter . 1999. What is SCADA? ( 1999 ). Axel Daneels and Wayne Salter. 1999. What is SCADA? (1999)."},{"key":"e_1_3_2_1_12_1","volume-title":"Enrique Blanco Vinuela, and Borja Fern\u00e1ndez Adiego","author":"Darvas D\u00e1niel","year":"2015","unstructured":"D\u00e1niel Darvas , Enrique Blanco Vinuela, and Borja Fern\u00e1ndez Adiego . 2015 . PLCverif: A tool to verify PLC programs based on model checking techniques. (2015). D\u00e1niel Darvas, Enrique Blanco Vinuela, and Borja Fern\u00e1ndez Adiego. 2015. PLCverif: A tool to verify PLC programs based on model checking techniques. (2015)."},{"key":"e_1_3_2_1_13_1","volume-title":"IEC 61131--3: programming industrial automation systems: concepts and programming languages, requirements for programming systems, decision-making aids","author":"John Karl Heinz","unstructured":"Karl Heinz John and Michael Tiegelkamp . 2010. IEC 61131--3: programming industrial automation systems: concepts and programming languages, requirements for programming systems, decision-making aids . Springer Science & Business Media . Karl Heinz John and Michael Tiegelkamp. 2010. IEC 61131--3: programming industrial automation systems: concepts and programming languages, requirements for programming systems, decision-making aids. Springer Science & Business Media."},{"key":"e_1_3_2_1_14_1","volume-title":"Guide to industrial control systems (ICS) security. NIST Special Publication 800--82 1 (June","author":"Keith Stouffer Karen Scarfone","year":"2011","unstructured":"Karen Scarfone Keith Stouffer , Joe Falco . 2011. Guide to industrial control systems (ICS) security. NIST Special Publication 800--82 1 (June 2011 ). Karen Scarfone Keith Stouffer, Joe Falco. 2011. Guide to industrial control systems (ICS) security. NIST Special Publication 800--82 1 (June 2011)."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.3103\/S014641161407013X"},{"key":"e_1_3_2_1_16_1","volume-title":"On verification of PLC-programs written in the LD-language. Modelirovanie i Analiz Informatsionnykh Sistem 19, 2","author":"Kuz'min Egor Vladimirovich","year":"2012","unstructured":"Egor Vladimirovich Kuz'min and Valery Anatolievich Sokolov . 2012. On verification of PLC-programs written in the LD-language. Modelirovanie i Analiz Informatsionnykh Sistem 19, 2 ( 2012 ), 138--144. Egor Vladimirovich Kuz'min and Valery Anatolievich Sokolov. 2012. On verification of PLC-programs written in the LD-language. Modelirovanie i Analiz Informatsionnykh Sistem 19, 2 (2012), 138--144."},{"key":"e_1_3_2_1_17_1","volume-title":"Mohammed Bani Younis, and Georg Frey","author":"Loeis Kingliana","year":"2005","unstructured":"Kingliana Loeis , Mohammed Bani Younis, and Georg Frey . 2005 . Application of symbolic and bounded model checking to the verification of logic control systems. In ETFA. Kingliana Loeis, Mohammed Bani Younis, and Georg Frey. 2005. Application of symbolic and bounded model checking to the verification of logic control systems. In ETFA."},{"key":"e_1_3_2_1_18_1","volume-title":"The temporal logic of reactive and concurrent systems: Specification","author":"Manna Zohar","unstructured":"Zohar Manna and Amir Pnueli . 2012. The temporal logic of reactive and concurrent systems: Specification . Springer Science & Business Media . Zohar Manna and Amir Pnueli. 2012. The temporal logic of reactive and concurrent systems: Specification. Springer Science & Business Media."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.10"},{"key":"e_1_3_2_1_20_1","volume-title":"Conference on Automated Deduction (CADE). 152--163","author":"Pavlovic Olivera","year":"2007","unstructured":"Olivera Pavlovic , Ralf Pinger , and Maik Kollmann . 2007 . Automated formal verification of PLC programs written in IL . In Conference on Automated Deduction (CADE). 152--163 . Olivera Pavlovic, Ralf Pinger, and Maik Kollmann. 2007. Automated formal verification of PLC programs written in IL. In Conference on Automated Deduction (CADE). 152--163."}],"event":{"name":"CODASPY '18: Eighth ACM Conference on Data and Application Security and Privacy","location":"Tempe AZ USA","acronym":"CODASPY '18","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the Eighth ACM Conference on Data and Application Security and Privacy"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3176258.3176949","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3176258.3176949","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:26:40Z","timestamp":1750213600000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3176258.3176949"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3,13]]},"references-count":20,"alternative-id":["10.1145\/3176258.3176949","10.1145\/3176258"],"URL":"https:\/\/doi.org\/10.1145\/3176258.3176949","relation":{},"subject":[],"published":{"date-parts":[[2018,3,13]]},"assertion":[{"value":"2018-03-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}