{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,7]],"date-time":"2026-03-07T02:27:01Z","timestamp":1772850421473,"version":"3.50.1"},"reference-count":70,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":["Proc. IEEE"],"published-print":{"date-parts":[[2018,1]]},"DOI":"10.1109\/jproc.2017.2725642","type":"journal-article","created":{"date-parts":[[2017,8,17]],"date-time":"2017-08-17T20:23:41Z","timestamp":1503001421000},"page":"129-143","source":"Crossref","is-referenced-by-count":46,"title":["ARMET: Behavior-Based Secure and Resilient Industrial Control Systems"],"prefix":"10.1109","volume":"106","author":[{"given":"Muhammad Taimoor","family":"Khan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dimitrios","family":"Serpanos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Howard","family":"Shrobe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref70","year":"0"},{"key":"ref39","first-page":"1","article-title":"On a decision method in restricted second-order arithmetic","author":"buechi","year":"1962","journal-title":"Proc Int Congress Logic Method Phil Sci"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19600060105"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/DSNW.2012.6264663"},{"key":"ref32","article-title":"Formal verification of stability properties of cyber-physical systems","author":"chan","year":"2016","journal-title":"Proc CoqPL"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/SOSCYPS.2016.7580000"},{"key":"ref30","first-page":"34","author":"anand","year":"2015","journal-title":"ROSCoq Robots Powered by Constructive Reals"},{"key":"ref37","first-page":"524","article-title":"Event calculus","volume":"1","author":"borchardt","year":"0","journal-title":"Proc 9th Int Joint Conf Artif Intell"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60630-0_5"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/2380656.2380677"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80066-4"},{"key":"ref60","author":"gary leavens","year":"2006","journal-title":"Design by Contract with JML"},{"key":"ref62","first-page":"48","article-title":"Joshua: Uniform access to heterogeneous knowledge structures or why joshing is better than conniving or planning","author":"rowley","year":"1987","journal-title":"Proc AAAI"},{"key":"ref61","first-page":"3","author":"goguen","year":"2000","journal-title":"Introducing OBJ"},{"key":"ref63","article-title":"Runtime monitoring for safety-critical embedded systems","author":"kane","year":"2015"},{"key":"ref28","article-title":"A constructive approach to the problem of program correctness","author":"dijkstra","year":"1967","journal-title":"Circulated Privately Tech Rep"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1109\/SMARTGRID.2010.5622046"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2015.7402610"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1109\/TSG.2011.2163807"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1109\/Allerton.2012.6483441"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2958736"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1109\/TSG.2011.2161892"},{"key":"ref68","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/978-3-642-31365-3_23","article-title":"$\\delta $ -Complete decision procedures for satisfiability over the reals","author":"gao","year":"2012","journal-title":"Proc 6th Int Joint Conf Autom Reasoning-(IJCAR)"},{"key":"ref69","year":"0"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/CPRE.2011.6035612"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/HICSS.2016.331"},{"key":"ref20","article-title":"Sound and complete runtime security monitor for application software","author":"khan","year":"2016"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/TSG.2012.2195338"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.2514\/1.I010201"},{"key":"ref24","first-page":"3153","article-title":"False data injection attacks with incomplete information against smart power grids","author":"rahman","year":"2012","journal-title":"Proc IEEE Global Commun Conf (GLOBECOM)"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2010.5717318"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/SmartGridComm.2013.6687993"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.4271\/2016-01-0019"},{"key":"ref51","first-page":"200","author":"kong","year":"2015","journal-title":"dReach $\\delta $ -Reachability Analysis for Hybrid Systems"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"ref58","first-page":"91","author":"adepu","year":"2016","journal-title":"Using Process Invariants to Detect Cyber Attacks on a Water Treatment System"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16277-0_6"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(90)90074-V"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.111.6"},{"key":"ref54","author":"borger","year":"2003","journal-title":"Abstract State Machines A Method for High-Level System Design and Analysis"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1016\/S0164-1212(02)00041-9"},{"key":"ref52","first-page":"826","article-title":"Software reliability via run-time result-checking","volume":"44","author":"blum","year":"1994","journal-title":"J ACM"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103669"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813669"},{"key":"ref40","first-page":"4","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"rabin","year":"1969","journal-title":"Trans Amer Math Soc"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.003"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.03.025"},{"key":"ref14","article-title":"Synthesis of correct-by-design schedulers for hybrid systems","author":"soulat","year":"2014"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/WF-IoT.2016.7845510"},{"key":"ref18","first-page":"1836","article-title":"AWDRAT: A cognitive middleware system for information survivability","volume":"2","author":"shrobe","year":"2006","journal-title":"Proc 18th Int Conf Innovat Appl Artif Intell"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511977619"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.14236\/ewic\/ICS2016.14"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2011.67"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2542049"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3029589"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1952982.1952995"},{"key":"ref7","first-page":"1","article-title":"Using model-based intrusion detection for scada networks","author":"cheung","year":"2007","journal-title":"Proc SCADA Security Sci Symp"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/WF-IoT.2016.7845513"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1966913.1966959"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/3052973.3053024"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/1297105.1297069"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn076"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1961-0139530-9"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90268-2"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.52"}],"container-title":["Proceedings of the IEEE"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/5\/8232482\/08011473.pdf?arnumber=8011473","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T10:22:57Z","timestamp":1659349377000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8011473\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1]]},"references-count":70,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/jproc.2017.2725642","relation":{},"ISSN":["0018-9219","1558-2256"],"issn-type":[{"value":"0018-9219","type":"print"},{"value":"1558-2256","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1]]}}}