SpringerLink
Log in

Robustness Verification of Deep Neural Networks Using Star-Based Reachability Analysis with Variable-Length Time Series Input

  • Conference paper
  • First Online:
Formal Methods for Industrial Critical Systems (FMICS 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14290))

Abstract

Data-driven, neural network (NN) based anomaly detection and predictive maintenance are emerging as important research areas. NN-based analytics of time-series data provide valuable insights and statistical evidence for diagnosing past behaviors and predicting critical parameters like equipment’s remaining useful life (RUL), state-of-charge (SOC) of batteries, etc. Unfortunately, input time series data can be exposed to intentional or unintentional noise when passing through sensors, making robust validation and verification of these NNs a crucial task. Using set-based reachability analysis, this paper presents a case study of the formal robustness verification approach for time series regression NNs (TSRegNN). It utilizes variable-length input data to streamline input manipulation and enhance network architecture generalizability. The method is applied to two data sets in the Prognostics and Health Management (PHM) application areas: (1) SOC estimation of a Lithium-ion battery and (2) RUL estimation of a turbine engine. Finally, the paper introduces several performance measures to evaluate the effect of bounded perturbations in the input on network outputs, i.e., future outcomes. Overall, the paper offers a comprehensive case study for validating and verifying NN-based analytics of time-series data in real-world applications, emphasizing the importance of robustness testing for accurate and reliable predictions, especially considering the impact of noise on future outcomes.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 49.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 64.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    The code is available at: https://github.com/verivital/nnv/tree/master/code/nnv/examples/Submission/FMICS2023.

  2. 2.

    Each feature is a measurable piece of data that is used for analysis.

  3. 3.

    A detailed version of this paper with example plots of noises, sample calculations for the robustness measures and the network architectures used can be found in [25].

  4. 4.

    The detailed version of this paper, available in [25], provides a comprehensive feature extraction method called ‘Prognosability’ that extracts 17 features out of the total 26 features for the TEDS dataset.

  5. 5.

    The MFAI noise, i.e., adding the \(L_\infty \) norm to all feature values across all time instances, significantly increases the input-set size compared to other noise types. This leads to computationally expensive calculations for layer-wise reachability, resulting in longer run times. Moreover, noise in an industrial setting affecting all features over an extended period is unlikely. Considering these factors, we decided to exclude the results of the MFAI noise for the TEDS dataset from our analysis.

References

  1. Predict battery state of charge using deep learning - MATLAB & ; Simulink – mathworks.com. https://www.mathworks.com/help/deeplearning/ug/predict-soc-using-deep-learning.html

  2. Prognostics center of excellence - data repository. https://ti.arc.nasa.gov/tech/dash/groups/pcoe/prognostic-data-repository/#turbofan

  3. Remaining useful life estimation using convolutional neural network - MATLAB & ; Simulink – mathworks.com. https://www.mathworks.com/help/predmaint/ug/remaining-useful-life-estimation-using-convolutional-neural-network.html

  4. Anderson, G., Pailoor, S., Dillig, I., Chaudhuri, S.: Optimization and abstraction: a synergistic approach for analyzing neural network robustness. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 731–744 (2019)

    Google Scholar 

  5. Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., Schilling, C.: JuliaReach: a toolbox for set-based reachability. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 39–44 (2019)

    Google Scholar 

  6. Borgi, T., Hidri, A., Neef, B., Naceur, M.S.: Data analytics for predictive maintenance of industrial robots. In: 2017 International Conference on Advanced Systems and Electric Technologies (IC_ASET), pp. 412–417. IEEE (2017)

    Google Scholar 

  7. Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., Misener, R.: Efficient verification of ReLU-based neural networks via dependency analysis. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, pp. 3291–3299 (2020)

    Google Scholar 

  8. DeLillo, D.: White noise. Penguin (1999)

    Google Scholar 

  9. EASA, Aerospace, C.: Formal methods use for learning assurance (formula). Tech. Rep. (2023)

    Google Scholar 

  10. Ferguson, C.E.: Time-series production functions and technological progress in American manufacturing industry. J. Polit. Econ. 73(2), 135–147 (1965)

    Article  Google Scholar 

  11. Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. ar**v preprint ar**v:1412.6572 (2014)

  12. Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443–452. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_26

    Chapter  Google Scholar 

  13. Kauffman, S., Dunne, M., Gracioli, G., Khan, W., Benann, N., Fischmeister, S.: Palisade: a framework for anomaly detection in embedded systems. J. Syst. Archit. 113, 101876 (2021)

    Article  Google Scholar 

  14. Kollmeyer, P., Vidal, C., Naguib, M., Skells, M.: LG 18650hg2 Li-ion battery data and example deep neural network xEV SOC estimator script. Mendeley Data 3, 2020 (2020)

    Google Scholar 

  15. Krizhevsky, A., Sutskever, I., Hinton, G.E.: ImageNet classification with deep convolutional neural networks. Advances in Neural Information Processing Systems, vol. 25 (2012)

    Google Scholar 

  16. Lawrence, S., Giles, C.L., Tsoi, A.C., Back, A.D.: Face recognition: a convolutional neural-network approach. IEEE Trans. Neural Netw. 8(1), 98–113 (1997)

    Article  Google Scholar 

  17. LeCun, Y., Bottou, L., Bengio, Y., Haffner, P.: Gradient-based learning applied to document recognition. Proc. IEEE 86(11), 2278–2324 (1998)

    Article  Google Scholar 

  18. Lin, C.Y., Hsieh, Y.M., Cheng, F.T., Huang, H.C., Adnan, M.: Time series prediction algorithm for intelligent predictive maintenance. IEEE Robot. Autom. Lett. 4(3), 2807–2814 (2019)

    Article  Google Scholar 

  19. Lopez, D.M., Choi, S.W., Tran, H.D., Johnson, T.T.: NNV 2.0: the neural network verification tool. In: International Conference on Computer Aided Verification, pp. 397–412. Springer (2023). https://doi.org/10.1007/978-3-031-37703-7_19

  20. Lv, F., Wen, C., Liu, M., Bao, Z.: Weighted time series fault diagnosis based on a stacked sparse autoencoder. J. Chemometr. 31(9), e2912 (2017)

    Article  Google Scholar 

  21. Martinez, C.M., Cao, D.: iHorizon-Enabled energy management for electrified vehicles. Butterworth-Heinemann (2018)

    Google Scholar 

  22. Mohapatra, J., Weng, T.W., Chen, P.Y., Liu, S., Daniel, L.: Towards verifying robustness of neural networks against a family of semantic perturbations. In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, pp. 244–252 (2020)

    Google Scholar 

  23. Moosavi-Dezfooli, S.M., Fawzi, A., Frossard, P.: DeepFool: a simple and accurate method to fool deep neural networks. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 2574–2582 (2016)

    Google Scholar 

  24. Müller, M.N., Brix, C., Bak, S., Liu, C., Johnson, T.T.: The third international verification of neural networks competition (VNN-comp 2022): summary and results. ar**v preprint ar**v:2212.10376 (2022)

  25. Pal, N., Lopez, D.M., Johnson, T.T.: Robustness verification of deep neural networks using star-based reachability analysis with variable-length time series input. ar**v preprint ar**v:2307.13907 (2023)

  26. Pearson, K.: LIII. On lines and planes of closest fit to systems of points in space. The London, Edinburgh, and Dublin philosophical magazine and journal of science 2(11), 559–572 (1901)

    Google Scholar 

  27. Priemer, R.: Introductory signal processing, vol. 6. World Scientific (1991)

    Google Scholar 

  28. Priemer, R.: Signals and signal processing. Introductory Signal Processing, pp. 1–9 (1991)

    Google Scholar 

  29. de Riberolles, T., Zou, Y., Silvestre, G., Lochin, E., Song, J.: Anomaly detection for ICS based on deep learning: a use case for aeronautical radar data. Ann. Telecommun., pp. 1–13 (2022)

    Google Scholar 

  30. Saxena, A., Goebel, K.: Turbofan engine degradation simulation data set. NASA Ames Prognostics Data Repository, pp. 1551–3203 (2008)

    Google Scholar 

  31. Semenick Alam, I.M., Sickles, R.C.: Time series analysis of deregulatory dynamics and technical efficiency: the case of the us airline industry. Int. Econ. Rev. 41(1), 203–218 (2000)

    Article  Google Scholar 

  32. Sivaraman, A., Farnadi, G., Millstein, T., Van den Broeck, G.: Counterexample-guided learning of monotonic neural networks. Adv. Neural. Inf. Process. Syst. 33, 11936–11948 (2020)

    Google Scholar 

  33. Soomro, K., Bhutta, M.N.M., Khan, Z., Tahir, M.A.: Smart city big data analytics: an advanced review. Wiley Interdisc. Rev.: Data Min. Knowl. Disc. 9(5), e1319 (2019)

    Google Scholar 

  34. Stübinger, J., Schneider, L.: Understanding smart city-a data-driven literature review. Sustainability 12(20), 8460 (2020)

    Article  Google Scholar 

  35. Susto, G.A., Beghi, A.: Dealing with time-series data in predictive maintenance problems. In: 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA), pp. 1–4. IEEE (2016)

    Google Scholar 

  36. Szegedy, C., et al.: Intriguing properties of neural networks. ar**v preprint ar**v:1312.6199 (2013)

  37. Touloumi, G., et al.: Analysis of health outcome time series data in epidemiological studies. Environ.: Official J. Int. Environ. Soc. 15(2), 101–117 (2004)

    Google Scholar 

  38. Tran, H.-D., Bak, S., **ang, W., Johnson, T.T.: Verification of deep convolutional neural networks using ImageStars. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 18–42. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53288-8_2

    Chapter  Google Scholar 

  39. Tran, H.-D., et al.: Star-based reachability analysis of deep neural networks. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. Star-based reachability analysis of deep neural networks., vol. 11800, pp. 670–686. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_39

    Chapter  Google Scholar 

  40. Tran, H.-D., et al.: Star-based reachability analysis of deep neural networks. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 670–686. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_39

    Chapter  Google Scholar 

  41. Tran, H.-D., et al.: Robustness verification of semantic segmentation neural networks using relaxed reachability. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 263–286. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-81685-8_12

    Chapter  Google Scholar 

  42. Tran, H.-D., et al.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 3–17. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53288-8_1

    Chapter  Google Scholar 

  43. Truax, B.: Handbook for acoustic ecology. Cambridge Street Records (1999)

    Google Scholar 

  44. Wang, Z., Wang, Y., Fu, F., Jiao, R., Huang, C., Li, W., Zhu, Q.: A tool for neural network global robustness certification and training. ar**v preprint ar**v:2208.07289 (2022)

  45. Zeger, S.L., Irizarry, R., Peng, R.D.: On time series analysis of public health and biomedical data. Annu. Rev. Public Health 27, 57–79 (2006)

    Article  Google Scholar 

  46. Zhang, Z., Lai, X., Wu, M., Chen, L., Lu, C., Du, S.: Fault diagnosis based on feature clustering of time series data for loss and kick of drilling process. J. Process Control 102, 24–33 (2021)

    Article  Google Scholar 

Download references

Acknowledgements

The material presented in this paper is based upon work supported by the National Science Foundation (NSF) through grant numbers 1910017, 2028001, 2220426, and 2220401, and the Defense Advanced Research Projects Agency (DARPA) under contract number FA8750-18-C-0089 and FA8750-23-C-0518, and the Air Force Office of Scientific Research (AFOSR) under contract number FA9550-22-1-0019 and FA9550-23-1-0135. Any opinions, findings, conclusions, or recommendations expressed in this paper are those of the authors and do not necessarily reflect the views of AFOSR, DARPA, or NSF. We also want to thank our colleagues, Tianshu and Bernie for their valuable feedback.

Author information

Authors and Affiliations

  1. Institute for Software Integrated Systems, Vanderbilt University, Nashville, TN, 37212, USA

    Neelanjana Pal, Diego Manzanas Lopez & Taylor T Johnson

Authors
  1. Neelanjana Pal
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Diego Manzanas Lopez
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Taylor T Johnson
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Neelanjana Pal .

Editor information

Editors and Affiliations

  1. Fondazione Bruno Kessler, Povo, Italy

    Alessandro Cimatti

  2. NASA Langley Research Center, AMA-NASA LaRC, Hampton, VA, USA

    Laura Titolo

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Pal, N., Lopez, D.M., Johnson, T.T. (2023). Robustness Verification of Deep Neural Networks Using Star-Based Reachability Analysis with Variable-Length Time Series Input. In: Cimatti, A., Titolo, L. (eds) Formal Methods for Industrial Critical Systems. FMICS 2023. Lecture Notes in Computer Science, vol 14290. Springer, Cham. https://doi.org/10.1007/978-3-031-43681-9_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-43681-9_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-43680-2

  • Online ISBN: 978-3-031-43681-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation