Advertisement

Towards ‘Verifying’ a Water Treatment System

  • Jingyi Wang
  • Jun Sun
  • Yifan Jia
  • Shengchao Qin
  • Zhiwu Xu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

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.

Notes

Acknowledgement

The work was supported in part by Singapore NRF Award No. NRF2014NCR-NCR001-40, NSFC projects 61772347, 61502308, STFSC project JCYJ20170302153712968.

References

  1. 1.
    Abeel, T., Van de Peer, Y., Saeys, Y.: Java-ml: a machine learning library. J. Mach. Learn. Res. 10, 931–934 (2009)MathSciNetzbMATHGoogle Scholar
  2. 2.
    Bass, R.F.: Stochastic Processes, vol. 33. Cambridge University Press, Cambridge (2011)CrossRefGoogle Scholar
  3. 3.
    Brázdil, T., et al.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98–114. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11936-6_8CrossRefGoogle Scholar
  4. 4.
    Carrasco, R.C., Oncina, J.: Learning stochastic regular grammars by means of a state merging method. In: Carrasco, R.C., Oncina, J. (eds.) ICGI 1994. LNCS, vol. 862, pp. 139–152. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58473-0_144CrossRefzbMATHGoogle Scholar
  5. 5.
    Chang, C.-C., Lin, C.-J.: Libsvm: a library for support vector machines. ACM Trans. Intell. Syst. Technol. (TIST) 2(3), 27 (2011)Google Scholar
  6. 6.
    Chen, Y., et al.: Learning Markov models for stationary system behaviors. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 216–230. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28891-3_22CrossRefGoogle Scholar
  7. 7.
    Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1–12. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-24372-1_1CrossRefzbMATHGoogle Scholar
  8. 8.
    Fiterău-Broştean, P., Janssen, R., Vaandrager, F.: Combining model learning and model checking to analyze TCP implementations. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 454–471. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41540-6_25CrossRefGoogle Scholar
  9. 9.
    Gao, S., Kong, S., Chen, W., Clarke, E.: Delta-complete analysis for bounded reachability of hybrid systems. arXiv preprint arXiv:1404.7171 (2014)
  10. 10.
    Goh, J., Adepu, S., Junejo, K.N., Mathur, A.: A dataset to support research in the design of secure water treatment systems. In: Havarneanu, G., Setola, R., Nassopoulos, H., Wolthusen, S. (eds.) CRITIS 2016. LNCS, vol. 10242, pp. 88–99. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-71368-7_8CrossRefGoogle Scholar
  11. 11.
    Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 170, pp. 265–292. Springer, Heidelberg (2000).  https://doi.org/10.1007/978-3-642-59615-5_13CrossRefGoogle Scholar
  12. 12.
    Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 162–175. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-70545-1_16CrossRefGoogle Scholar
  13. 13.
    Jegourel, C., Sun, J., Dong, J.S.: Sequential schemes for frequentist estimation of properties in statistical model checking. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 333–350. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66335-7_23CrossRefGoogle Scholar
  14. 14.
    Kim, J., Kim, H., Lakshmanan, K., Rajkumar, R.R.: Parallel scheduling for cyber-physical systems: analysis and case study on a self-driving car. In: Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems, pp. 31–40. ACM (2013)Google Scholar
  15. 15.
    Kong, P., Li, Y., Chen, X., Sun, J., Sun, M., Wang, J.: Towards concolic testing for hybrid systems. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 460–478. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-48989-6_28CrossRefGoogle Scholar
  16. 16.
    Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. RV 10, 122–135 (2010)Google Scholar
  17. 17.
    Lin, J., Sedigh, S., Miller, A.: Towards integrated simulation of cyber-physical systems: a case study on intelligent water distribution. In: 2009 Eighth IEEE International Conference on Dependable, Autonomic and Secure Computing, DASC 2009, pp. 690–695. IEEE (2009)Google Scholar
  18. 18.
    Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning Markov decision processes for model checking. arXiv preprint arXiv:1212.3873 (2012)
  19. 19.
    Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning deterministic probabilistic automata from a model checking perspective. Mach. Learn. 105(2), 255–299 (2016)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Mathur, A.P., Tippenhauer, N.O.: SWaT: a water treatment testbed for research and training on ICS security. In: 2016 International Workshop on Cyber-Physical Systems for Smart Water Networks (CySWater), pp. 31–36. IEEE (2016)Google Scholar
  21. 21.
    Misra, S., Krishna, P.V., Saritha, V., Obaidat, M.S.: Learning automata as a utility for power management in smart grids. IEEE Commun. Mag. 51(1), 98–104 (2013)CrossRefGoogle Scholar
  22. 22.
    Niggemann, O., Stein, B., Vodencarevic, A., Maier, A., Büning, H.K.: Learning behavior models for hybrid timed systems. AAAI 2, 1083–1090 (2012)Google Scholar
  23. 23.
    Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14509-4CrossRefzbMATHGoogle Scholar
  24. 24.
    Ron, D., Singer, Y., Tishby, N.: The power of amnesia: learning probabilistic automata with variable memory length. Mach. Learn. 25(2–3), 117–149 (1996)CrossRefGoogle Scholar
  25. 25.
    Sen, K., Viswanathan, M., Agha, G.: Learning continuous time Markov chains from sample executions. In: Proceedings of the 2004 First International Conference on the Quantitative Evaluation of Systems, QEST 2004, pp. 146–155. IEEE (2004)Google Scholar
  26. 26.
    Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27813-9_16CrossRefGoogle Scholar
  27. 27.
    SUTD: Swat dataset website. https://itrust.sutd.edu.sg/dataset/
  28. 28.
  29. 29.
    Wachter, B., Zhang, L., Hermanns, H.: Probabilistic model checking modulo theories. In: Fourth International Conference on the Quantitative Evaluation of Systems, pp. 129–140. IEEE (2007)Google Scholar
  30. 30.
    Wang, J.: Ziqian website. https://github.com/wang-jingyi/Ziqian
  31. 31.
    Wang, J., Chen, X., Sun, J., Qin, S.: Improving probability estimation through active probabilistic model learning. In: Duan, Z., Ong, L. (eds.) ICFEM 2017. LNCS, vol. 10610, pp. 379–395. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-68690-5_23CrossRefGoogle Scholar
  32. 32.
    Wang, J., Sun, J., Qin, S.: Verifying complex systems probabilistically through learning, abstraction and refinement. CoRR, abs/1610.06371 (2016)Google Scholar
  33. 33.
    Wang, J., Sun, J., Yuan, Q., Pang, J.: Should we learn probabilistic models for model checking? A new approach and an empirical study. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 3–21. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54494-5_1CrossRefGoogle Scholar
  34. 34.
    Wang, J., Sun, J., Yuan, Q., Pang, J.: Learning probabilistic models for model checking: an evolutionary approach and an empirical study. In: Int. J. Softw. Tools Technol. Transf., 1–16 (2018).  https://doi.org/10.1007/s10009-018-0492-7
  35. 35.
    Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon (2005)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Singapore University of Technology and DesignSingaporeSingapore
  2. 2.School of Computing, Media and the ArtsTeesside UniversityMiddlesbroughUK
  3. 3.College of Computer Science and Software EngineeringShenzhen UniversityShenzhenChina
  4. 4.TUV-SUD Asia Pacific Pte Ltd.SingaporeSingapore

Personalised recommendations