Model Checking - Case Study of a Temporary Structures Monitoring System

Dongpeng Xu, Xiao Yuan, Dinghao Wu, Chimay J. Anumba

Research output: Chapter in Book/Report/Conference proceedingChapter

1 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationCyber-Physical Systems in the Built Environment
PublisherSpringer International Publishing
Number of pages21
ISBN (Electronic)9783030415600
ISBN (Print)9783030415594
StatePublished - Jan 1 2020

All Science Journal Classification (ASJC) codes

  • General Engineering
  • General Arts and Humanities
  • General Environmental Science

Cite this