Model Checking - Case Study of a Temporary Structures Monitoring System

Model checking is a formal method for verifying system properties by checking whether a model meets a given specification. This involves using appropriate symbolic algorithms to traverse the model and check if the specifications, typically expressed as temporal logic formulas, are met. The effectiveness of cyber-physical systems is dependent largely on how well the cyber and physical elements work together. In such systems, any inconsistencies in the system model could result in either failure or unintended consequences. In this chapter, we present a case study of the model checking of a CPS-based temporary structures monitoring system. We use model checking to try to detect the vulnerabilities in the system. The case study shows that model checking can identify vulnerabilities in a CPS-based system and help developers fix the vulnerabilities.