Publication Type

Conference Proceeding Article

Version

acceptedVersion

Publication Date

7-2018

Abstract

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.

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

International Symposium on Formal Methods: 22nd FM 2018, Oxford, July 15-17: Proceedings

Volume

10951

First Page

1

Last Page

18

ISBN

9783319955810

Identifier

10.1007/978-3-319-95582-7_5

Publisher

Springer

City or Country

Cham

Additional URL

https://doi.org/10.1007/978-3-319-95582-7_5

Download

Share

COinS