Using Finite State Machines and Model Checking to Identify Cyber-Attack Vulnerabilities in Water Distribution Systems

Abstract Cyber water distribution systems (CWDSs) couple physical and cyber components, creating vulnerabilities to cyber attacks, as intruders can infiltrate and disrupt systems through network-connected devices. This research demonstrates a formal methods approach to identify vulnerabilities in CWDSs through model checking , which is an automatic verification technique for finite state systems. A finite state machine model of a CWDS is developed, and the Labelled Transition System Analyser is applied to check safety properties and identify vulnerabilities for attack scenarios. The approach is applied for a small example system to identify vulnerabilities in cyber elements. Consequences for the pipe network are evaluated, revealing the vulnerabilities that can be exploited to empty a water tank within the system. This research demonstrates the use of model checking tools to identify vulnerabilities in CWDSs.