Improving Verification Accuracy of CPS by Modeling and Calibrating Interaction Uncertainty

Abstract

Cyber-Physical Systems (CPS) intrinsically combine hardware and physical systems with software and network, which are together creating complex and correlated interactions. CPS applications often experience uncertainty in interacting with environment through unreliable sensors. They can be faulty and exhibit runtime errors if developers have not considered environmental interaction uncertainty adequately. Existing work in verifying CPS applications ignores interaction uncertainty and thus may overlook uncertainty-related faults. To improve verification accuracy, in this article we propose a novel approach to verifying CPS applications with explicit modeling of uncertainty arisen in the interaction between them and the environment. Our approach builds an Interactive State Machine network for a CPS application and models interaction uncertainty by error ranges and distributions. Then it encodes both the application and uncertainty models to Satisfiability Modulo Theories (SMT) formula to leverage SMT solvers searching for counterexamples that represent application failures. The precision of uncertainty model can affect the verification results. However, it may be difficult to model interaction uncertainty precisely enough at the beginning, because of the uncontrollable noise of sensors and insufficient data sample size. To further improve the accuracy of the verification results, we propose an approach to identifying and calibrating imprecise uncertainty models. We exploit the inconsistency between the counterexamples’ estimate and actual occurrence probabilities to identify possible imprecision in uncertainty models, and the calibration of imprecise models is to minimize the inconsistency, which is reduced to a Search-Based Software Engineering problem. We experimentally evaluated our verification and calibration approaches with real-world CPS applications, and the experimental results confirmed their effectiveness and efficiency.

References

1. Sara Abbaspour Asadollah, Rafia Inam, and Hans Hansson. 2015. A Survey on Testing for Cyber Physical System. Springer, Cham, 194--207.
2. Ravi Akella and Bruce M. McMillin. 2009. Model-checking BNDC properties in cyber-physical systems. In Proceedings of the 2009 33rd Annual IEEE International Computer Software and Applications Conference (COMPSAC’09). IEEE Computer Society, Washington, DC, 660--663.
3. S. Ali and T. Yue. 2015. U-Test: Evolving, modelling and testing realistic uncertain behaviours of cyber-physical systems. In Proceedings of the 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST’15). 1--2.
4. Cesare Alippi. 2014. Intelligence for Embedded Systems. Springer, Berlin.
5. Christel Baier, Joost-Pieter Katoen, and others. 2008. Principles of Model Checking. MIT Press, Cambridge.
6. A. Banerjee, K. K. Venkatasubramanian, T. Mukherjee, and S. K. S. Gupta. 2012. Ensuring safety, security, and sustainability of mission-critical cyber-physical systems. Proc. IEEE 100, 1 ( Jan. 2012), 283--299.
7. M. M. Bersani and M. García-Valls. 2016. The cost of formal verification in adaptive CPS. An example of a virtualized server node. In Proceedings of the 2016 IEEE 17th International Symposium on High Assurance Systems Engineering (HASE’16). 39--46.
8. Keith Beven and Andrew Binley. 1992. The future of distributed models: Model calibration and uncertainty prediction. Hydrol. Process. 6, 3 (1992), 279--298.
9. David Broman, Edward A. Lee, Stavros Tripakis, and Martin Törngren. 2012. Viewpoints, formalisms, languages, and tools for cyber-physical systems. In Proceedings of the 6th International Workshop on Multi-Paradigm Modeling (MPM’12). ACM, New York, NY, 49--54.
10. Betty H. C. Cheng, Pete Sawyer, Nelly Bencomo, and Jon Whittle. A goal-based modeling approach to develop requirements of an adaptive system with environmental uncertainty. In Proceedings of the 12th International Conference on Model Driven Engineering Languages and Systems (MODELS). LNCS, Vol. 5795. Springer, Berlin, 468--483.
11. Edmund M. Clarke and Paolo Zuliani. 2011. Statistical model checking for cyber-physical systems. In Proceedings of the 9th International Conference on Automated Technology for Verification and Analysis (ATVA’11). Springer-Verlag, Berlin, 1--12. http://dl.acm.org/citation.cfm?id=2050917.2050919.
12. Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08), C. R. Ramakrishnan and Jakob Rehof (Eds.). 337--340.
13. Sebastian Elbaum and David S. Rosenblum. 2014. Known unknowns: Testing in the presence of uncertainty. In Proceedings of the Symposium on the Foundations of Software Engineering (FSE’14). Hong Kong, China, 833--836.
14. Marisol García-Valls and Roberto Baldoni. 2015. Adaptive middleware design for CPS: Considerations on the OS, resource managers, and the network run-time. In Proceedings of the 14th International Workshop on Adaptive and Reflective Middleware (ARM’15). ACM, New York, NY, 3:1--3:6.
15. Marisol García-Valls, Christian Calva-Urrego, Juan A. de la Puente, and Alejandro Alonso. 2017. Adjusting middleware knobs to assess scalability limits of distributed cyber-physical systems. Comput. Stand. Interfaces 51 (2017), 95--103.
16. Marisol García-Valls, Diego Perez-Palacin, and Raffaela Mirandola. 2014. Time-sensitive adaptation in CPS through run-time configuration generation and verification. In Proceedings of the 2014 IEEE 38th Annual Computer Software and Applications Conference (COMPSAC’14). IEEE Computer Society, 332--337.
17. Andrew Gelman, B. Carlin John, S. Stern Hal, and Donald B. Rubin. 2014. Bayesian Data Analysis. Chapman 8 Hall/CRC Press.
18. Herman Geuvers, Adam Koprowski, Dan Synek, and Eelis van der Weegen. 2010. Automated machine-checked hybrid system safety proofs. In Proceedings of the 1st International Interactive Theorem Proving (ITP’10), Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer, Berlin, 259--274.
19. David E. Goldberg. 1989. Genetic Algorithms in Search, Optimization and Machine Learning (1st ed.). Addison-Wesley Longman, Boston, MA.
20. Mark Harman, Phil McMinn, Jerffeson Teixeira de Souza, and Shin Yoo. 2012. Search based software engineering: Techniques, taxonomy, tutorial. In Proceedings of the International Summer Schools of Empirical Software Engineering and Verification (LASER 2008-2010), Bertrand Meyer and Martin Nordio (Eds.). Springer, Berlin, 1--59.
21. J. He, Y. Geng, Y. Wan, S. Li, and K. Pahlavan. 2013. A cyber physical test-bed for virtualization of RF access environment for body sensor network. IEEE Sens. J. 13, 10 (Oct. 2013), 3826--3836.
22. T. A. Henzinger, Pei-Hsin Ho, and H. Wong-Toi. 1995. HYTECH: The next generation. In Proceedings of the 16th IEEE Real-Time Systems Symposium. 56--65.
23. John H. Holland. 1975. Adaptation in Natural and Artificial Systems. University of Michigan Press.
24. Huang-Ming Huang, Terry Tidwell, Christopher Gill, Chenyang Lu, Xiuyu Gao, and Shirley Dyke. 2010. Cyber-physical systems for real-time hybrid structural testing: A case study. In Proceedings of the 1st ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS’10). ACM, New York, NY, 69--78.
25. Chii-Ruey Hwang. 1988. Simulated annealing: Theory and applications. Acta Appl. Math. 12, 1 (1988), 108--111.
26. Aaron Kane, Thomas Fuhrman, and Philip Koopman. 2014. Monitor based oracles for cyber-physical system testing: Practical experience report. In Proceedings of the 2014 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN’14). IEEE Computer Society, Washington, DC, 148--155.
27. S. Kirkpatrick, C. D. Gelatt, and M. P. Vecchi. 1983. Optimization by simulated annealing. Science 220, 4598 (1983), 671--680. arXiv: http://science.sciencemag.org/content/220/4598/671.full.pdf
28. P. Kumar, D. Goswami, S. Chakraborty, A. Annaswamy, K. Lampka, and L. Thiele. 2012. A hybrid approach to cyber-physical systems verification. In Proceedings of the ACM/EDAC/IEEE Design Automation Conference (DAC’12). 688--696.
29. L. S. Lasdon, A. D. Waren, A. Jain, and M. Ratner. 1978. Design and testing of a generalized reduced gradient code for nonlinear programming. ACM Trans. Math. Softw. 4, 1 (Mar. 1978), 34--50.
30. E. A. Lee. 2008. Cyber physical systems: Design challenges. In Proceedings of the 2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC’08). 363--369.
31. Jian Lü, Yu Huang, Chang Xu, and Xiaoxing Ma. 2013. Theories of Programming and Formal Methods. Springer-Verlag, Berlin, 271--284. http://dl.acm.org/citation.cfm?id=2554641.2554658
32. Jian Lü, Xiaoxing Ma, Yu Huang, Chun Cao, and Feng Xu. 2009. Internetware: A shift of software paradigm. In Proceedings of the 1st Asia-Pacific Symposium on Internetware (Internetware’09). ACM, New York, NY, 7:1--7:9.
33. Atif Mashkoor and Osman Hasan. 2012. Formal Probabilistic Analysis of Cyber-Physical Transportation Systems. Springer, Berlin, 419--434.
34. MathWorks. 2017. MATLAB. Retrieved from http://www.mathworks.com/.
35. H. Mei, G. Huang, and T. Xie. 2012. Internetware: A software paradigm for internet computing. Computer 45, 6 (Jun. 2012), 26--31.
36. S. Mitra, T. Wongpiromsarn, and R. M. Murray. 2013. Verifying cyber-physical interactions in safety-critical systems. IEEE Secur. Priv. 11, 4 (Jul. 2013), 28--37.
37. Jorge J. Moré and D. C. Sorensen. 1983. Computing a trust region step. SIAM J. Sci. Statist. Comput. 4, 3 (1983), 553--572.
38. John Neter, Michael H. Kutner, Christopher J. Nachtsheim, and William Wasserman. 1996. Applied Linear Statistical Models. Vol. 4. Irwin, Chicago, IL.
39. Ragunathan Rajkumar, Insup Lee, Lui Sha, and John Stankovic. 2010. Cyber-physical systems: The next computing revolution. In Proceedings of the 47th Design Automation Conference (DAC’10). ACM, New York, NY, 731--736.
40. Singiresu S. Rao and S. S. Rao. 2009. Engineering Optimization: Theory and Practice. John Wiley 8 Sons, New York, NY.
41. D. Ricketts, G. Malecha, M. M. Alvarez, V. Gowda, and S. Lerner. 2015. Towards verification of hybrid systems in a foundational proof assistant. In Proceedings of the 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE’15). 248--257.
42. D. E. Rumelhart, G. E. Hinton, and R. J. Williams. 1986. Parallel Distributed Processing: Explorations in the Microstructure of Cognition, Vol. 1. MIT Press, Cambridge, MA, 318--362.
43. Stuart Jonathan Russell, Peter Norvig, John F. Canny, Jitendra M. Malik, and Douglas D. Edwards. 2003. Artificial Intelligence: A Modern Approach, Vol. 2. Prentice--Hall, Upper Saddle River, NJ.
44. Muhammad Usman Sanwal and Osman Hasan. 2013. Formal Verification of Cyber-Physical Systems: Coping with Continuous Elements. Springer, Berlin, 358--371.
45. Mary C. Seiler and Fritz A. Seiler. 1989. Numerical recipes in C: The art of scientific computing. Risk Anal. 9, 3 (1989), 415--416.
46. Joseph Sifakis and Sergio Yovine. 1996. Compositional specification of timed systems. In Annual Symposium on Theoretical Aspects of Computer Science. Springer, 345--359.
47. Lenardo C. Silva, Mirko Perkusich, Frederico M. Bublitz, Hyggo O. Almeida, and Angelo Perkusich. 2014. A model-based architecture for testing medical cyber-physical systems. In Proceedings of the 29th Annual ACM Symposium on Applied Computing (SAC’14). ACM, New York, NY, 25--30.
48. J. A. K. Suykens and J. Vandewalle. 1999. Least squares support vector machine classifiers. Neur. Process. Lett. 9, 3 (1999), 293--300.
49. P. Tabuada, S. Y. Caliskan, M. Rungger, and R. Majumdar. 2014. Towards robustness for cyber-physical systems. IEEE Trans. Automat. Contr. 59, 12 (Dec. 2014), 3151--3163.
50. T. Tidwell, X. Gao, H. M. Huang, C. Lu, S. Dyke, and C. Gill. 2009. Towards configurable real-time hybrid structural testing: A cyber-physical system approach. In Proceedings of the 2009 IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing. 37--44.
51. Tazio Vanni, Jonathan Karnon, Jason Madan, Richard G. White, W. John Edmunds, Anna M. Foss, and Rosa Legood. 2011. Calibrating models in economic evaluation. PharmacoEconom. 29 (Jan. 2011), 35--49.
52. Allan J. Volponi. 1994. Sensor error compensation in engine performance diagnostics. In Proceedings of the ASME 1994 International Gas Turbine and Aeroengine Congress and Exposition. American Society of Mechanical Engineers, V005T15A008.
53. Darrell Whitley. 1994. A genetic algorithm tutorial. Stat. Comput. 4, 2 (1994), 65--85.
54. Fang-Jing Wu, Yu-Fen Kao, and Yu-Chee Tseng. 2011. From wireless sensor networks towards cyber physical systems. Pervas. Mobile Comput. 7, 4 (2011), 397--413.
55. Chang Xu, Wenhua Yang, Xiaoxing Ma, Chun Cao, and Jian Lu. 2013. Environment rematching: Toward dependability improvement for self-adaptive applications. In Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering (ASE’13). 592--597.
56. Wenhua Yang, Chang Xu, Yepang Liu, Chun Cao, Xiaoxing Ma, and Jian Lu. 2014. Verifying Self-adaptive applications suffering uncertainty. In Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering (ASE’14). ACM, New York, NY, 199--210.
57. Lichen Zhang, Jifeng He, and Wensheng Yu. 2013. Test case generation from formal models of cyber physical system. Int. J. Hybrid Inf. Technol. 6, 3 (2013), 15--24.
58. Man Zhang, Bran Selic, Shaukat Ali, Tao Yue, Oscar Okariz, and Roland Norgren. 2016. Understanding uncertainty in cyber-physical systems: A conceptual model. In Proceedings of the 12th European Conference on Modelling Foundations and Applications (ECMFA’16), Andrzej Wąsowski and Henrik Lönn (Eds.). Springer, Cham, 247--264.
59. X. Zheng. 2014. Physically informed assertions for cyber physical systems development and debugging. In Proceedings of the 2014 IEEE International Conference on Pervasive Computing and Communication Workshops (PERCOM WORKSHOPS’14). 181--183.

Index Terms

• Computer systems organization

  • Embedded and cyber-physical systems

• Software and its engineering

  • Software creation and management

    • Software verification and validation