Cyber-physical systems (CPS) are networked systems that combine distributed computing systems to monitor and control the physical environment. CPS interacts with the environment using actuators and sensors by a means of computation, communication, and control. Over the years, there has been a significant increase in the attacks against CPS. Some of the attacks grant attackers a read or write access to the sensors or actuators, thereby dragging a sound CPS to an unsafe state. The success of attacks on CPS depends mainly on three factors: the timing of the attack, the duration of the attack, and an attacker’s knowledge about the target system. One of the most important aspects of CPS is to verify that the system satisfies its safety, timing, liveness and reachability properties with some level of confidence. It is imperative to note that any violations due to attacks or system failure poses physical consequences that could lead to catastrophic damages. In Critical cyber-physical systems where safety is paramount, thus the need for formal modeling and verification in building a robust and resilient CPS is great. In this work, we explored different formal approaches to reason about CPS’s behavior in the case of a Denial of Service or integrity attacks on sensors and actuators.
Dr. Hoda Mehrpouyan (Chair), Dr. Jidong Xiao, Dr. Michael Ekstrand, Mr. Stephen J. Reese, Dr. Jyh-haw Yeh (CompEE)