Towards ‘verifying’ a water treatment system

Jingyi Wang, Jun Sun, Yifan Jia, Shengchao Qin, Zhiwu Xu

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Modeling and verifying real-world cyber-physical systems is challenging, which is especially so for complex systems where manually modeling is infeasible. In this work, we report our experience on combining model learning and abstraction refinement to analyze a challenging system, i.e., a real-world Secure Water Treatment system (SWaT). Given a set of safety requirements, the objective is to either show that the system is safe with a high probability (so that a system shutdown is rarely triggered due to safety violation) or not. As the system is too complicated to be manually modeled, we apply latest automatic model learning techniques to construct a set of Markov chains through abstraction and refinement, based on two long system execution logs (one for training and the other for testing). For each probabilistic safety property, we either report it does not hold with a certain level of probabilistic confidence, or report that it holds by showing the evidence in the form of an abstract Markov chain. The Markov chains can subsequently be implemented as runtime monitors in SWaT.
Original languageEnglish
Title of host publicationFormal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
EditorsKlaus Havelund, Bill Roscoe, Erik de Vink, Jan Peleska
PublisherSpringer Verlag
Number of pages20
ISBN (Print)9783319955810
Publication statusPublished - 12 Jul 2018
EventInternational Symposium on Formal Methods 2018 - Oxford, United Kingdom
Duration: 15 Jul 201817 Jul 2018

Publication series

NameLecture Notes in Computer Science
Volume10951 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Symposium on Formal Methods 2018
Abbreviated titleFM: 2018
Country/TerritoryUnited Kingdom


Dive into the research topics of 'Towards ‘verifying’ a water treatment system'. Together they form a unique fingerprint.

Cite this