Underminer: A Framework for Automatically Identifying Nonconverging Behaviors in Black-Box System Models

Abstract

Evaluation of industrial embedded control system designs is a time-consuming and imperfect process. While an ideal process would apply a formal verification technique such as model checking or theorem proving, these techniques do not scale to industrial design problems, and it is often difficult to use these techniques to verify performance aspects of control system designs, such as stability or convergence. For industrial designs, engineers rely on testing processes to identify critical or unexpected behaviors. We propose a novel framework called Underminer to improve the testing process; this is an automated technique to identify nonconverging behaviors in embedded control system designs. Underminer treats the system as a black box and lets the designer indicate the model parameters, inputs, and outputs that are of interest. It differentiates convergent from nonconvergent behaviors using Convergence Classifier Functions (CCFs).

The tool can be applied in the context of testing models created late in the controller development stage, where it assumes that the given model displays mostly convergent behavior and learns a CCF in an unsupervised fashion from such convergent model behaviors. This CCF is then used to guide a thorough exploration of the model with the help of optimization-guided techniques or adaptive sampling techniques, with the goal of identifying rare nonconvergent model behaviors. Underminer can also be used early in the development stage, where models may have some significant nonconvergent behaviors. Here, the framework permits designers to indicate their mental model for convergence by labeling behaviors as convergent/nonconvergent and then constructs a CCF using a supervised learning technique. In this use case, the goal is to use the CCF to test an improved design for the model. Underminer supports a number of convergence-like notions, such as those based on Lyapunov analysis and temporal logic, and also CCFs learned directly from labeled output behaviors using machine-learning techniques such as support vector machines and neural networks. We demonstrate the efficacy of Underminer by evaluating its performance on several academic as well as industrial examples.

References

1. Y. S. R. Annapureddy, C. Liu, G. E. Fainekos, and S. Sankaranarayanan. 2011. S-TaLiRo: A tool for temporal logic falsification for hybrid systems. In TACAS. 254--257.
2. A. Balkan. 2017. Labeling for Not Stable System. Retrieved from http://www.cyphylab.ee.ucla.edu/labelingnotstablesystem/.
3. A. Balkan, J. Deshmukh, J. Kapinski, and P. Tabuada. 2015. Simulation-guided contraction analysis. In Proc. of the 1st Indian Control Conference. 71--75.
4. A. Balkan, P. Tabuada, J. V. Deshmukh, X. Jin, and J. Kapinski. 2016. Underminer: A framework for automatically identifying non-converging behaviors in black box system models. In 2016 International Conference on Embedded Software (EMSOFT’16). 7:1--7:10.
5. R. Bobiti and M. Lazar. 2015. A delta-sampling verification theorem for discrete-time, possibly discontinuous systems. In HSCC. 140--148.
6. C. Cortes and V. Vapnik. 1995. Support-vector networks. Mach. Learn. 20, 3 (Sept. 1995), 273--297.
7. T. Dang and T. Nahhal. 2009. Coverage-guided test generation for continuous and hybrid systems. Formal Methods Syst. Design 34, 2 (2009), 183--213.
8. A. Donzé. 2010. Breach, a toolbox for verification and parameter synthesis of hybrid systems. In CAV. 167--170.
9. A. Donzé and O. Maler. 2010. Robust satisfaction of temporal logic over real-valued signals. In FORMATS. 92--106.
10. T. Dreossi, T. Dang, A. Donzé, J. Kapinski, X. Jin, and J. V. Deshmukh. 2015. Efficient guiding strategies for testing of temporal properties of hybrid systems. In NASA Formal Methods. 127--142.
11. G. E. Fainekos and G. J. Pappas. 2009. Robustness of temporal logic specifications for continuous-time signals. Theor. Comp. Sci. 410, 42 (2009), 4262--4291.
12. R. Geiselhart, R. H. Gielen, M. Lazar, and F. R. Wirth. 2014. An alternative converse Lyapunov theorem for discrete-time systems. Syst. Control Lett. 70 (2014), 49--59.
13. S. Haykin. 1998. Neural Networks: A Comprehensive Foundation (2nd ed.). Prentice Hall PTR, Upper Saddle River, NJ.
14. M. Huang, K. Zaseck, K. Butts, and I. Kolmanovsky. 2016. Rate-based model predictive controller for diesel engine air path: Design and experimental evaluation. IEEE Trans. Control Syst. Technol. 99 (2016), 1--14.
15. ILOG. 2006. ILOG CPLEX: High-performance software for mathematical programming and optimization. Retrieved from http://www.ilog.com/products/cplex/.
16. X. Jin, J. V. Deshmukh, J. Kapinski, K. Ueda, and K. Butts. 2014. Powertrain control verification benchmark. In HSCC. 253--262.
17. A. Jones, Z. Kong, and C. Belta. 2014. Anomaly detection in cyber-physical systems: A formal methods approach. In CDC. 848--853.
18. J. Kapinski, J. V. Deshmukh, S. Sankaranarayanan, and N. Aréchiga. 2014. Simulation-guided lyapunov analysis for hybrid dynamical systems. In HSCC.
19. H. K. Khalil. 2002. Nonlinear Systems. Prentice Hall.
20. Z. Kong, A. Jones, A. M. Ayala, E. A. Gol, and C. Belta. 2014. Temporal logic inference for classification and prediction from data. In HSCC. 273--282.
21. A. Kozarev, J. Quindlen, J. How, and U. Topcu. 2016. Case studies in data-driven verification of dynamical systems. In HSCC.
22. V. Lakshmikantham, S. Leela, and A. A. Martynyuk. 1990. Practical Stability of Nonlinear Systems. World Scientific.
23. H. W. Lenstra. 1983. Integer programming with a fixed number of variables. Math. Oper. Res. 8, 4 (1983), 538--548.
24. J. Lofberg. 2004. YALMIP: A toolbox for modeling and optimization in MATLAB. In 2004 IEEE International Conference on Robotics and Automation (IEEE Cat. No.04CH37508). 284--289.
25. O. Maler and D. Nickovic. 2004. Monitoring temporal properties of continuous signals. In FORMATS. 152--166.
26. Mathworks. 2007. Using Simulink. MathWorks.
27. R. Medhat, S. Ramesh, B. Bonakdarpour, and S. Fischmeister. 2015. A framework for mining hybrid automata from input/output traces. In International Conference on Embedded Software (EMSOFT’15).
28. B. Messner and D. Tilbury. Control Tutorials for MATLAB and Simulink. Retrieved from http://ctms.engin.umich.edu/.
29. J. A. Nelder and R. Mead. 1965. A simplex method for function minimization. Comput. J. 7 (1965), 308--313.
30. S. Shankar Sastry. 1999. Nonlinear Systems: Analysis, Stability, and Control. Springer, New York.
31. K. C. Toh, M. J. Todd, and R. H. Tutuncu. 1998. SDPT3 - A MATLAB software package for semidefinite programming. Optim. Methods Softw. 11 (1998), 545--581.
32. U. Topcu, P. Seiler, and A. Packard. 2008. Local stability analysis using simulations and sum-of-squares programming. Automatica 44 (2008), 2669--2675.
33. J. Wiens, E. Horvitz, and J. V. Guttag. 2012. Patient risk stratification for hospital-associated C. diff as a time-series classification task. In Advances in Neural Information Processing Systems 25, F. Pereira, C. J. C. Burges, L. Bottou, and K. Q. Weinberger (Eds.). Curran Associates, 467--475. Retrieved from http://papers.nips.cc/paper/4525-patient-risk-stratification-for-hospital-associated-c-diff-as-a-time-series-classification-task.pdf.

Index Terms

• Computer systems organization

  • Embedded and cyber-physical systems

    • Embedded systems

      • Embedded software

• Computing methodologies

  • Machine learning

    • Learning paradigms

      • Supervised learning

        • Supervised learning by classification

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Software defect analysis

        • Software testing and debugging