Skip to main content
SpringerLink
Log in

Data-Driven Safety Verification of Complex Cyber-Physical Systems

  • Chapter
  • First Online:
Design Automation of Cyber-Physical Systems

  • 1128 Accesses

Abstract

Data-driven verification methods utilize execution data together with models for establishing safety requirements. These are often the only tools available for analyzing complex, nonlinear cyber-physical systems, for which purely model-based analysis is currently infeasible. In this chapter, we outline the key concepts and algorithmic approaches for data-driven verification and discuss the guarantees they provide. We introduce some of the software tools that embody these ideas and present several practical case studies demonstrating their application in safety analysis of autonomous vehicles, advanced driver assist systems (ADAS), satellite control, and engine control systems.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Autonomous systems sometimes also have incomplete requirements. The black-box approach described here does not address that problem.

  2. 2.

    ADAS stands for advanced driving assistance systems such as adaptive cruise control, automatic emergency braking, etc.

  3. 3.

    We prefer to present the learning question in this form as opposed to the one where we learn a Boolean concept because it is closer to the task at hand.

  4. 4.

    C2E2 available from:http://publish.illinois.edu/c2e2-tool/.

  5. 5.

    DryVR available from:https://gitlab.engr.illinois.edu/dryvrgroup/dryvrtool.

References

  1. Abbas, H., & Fainekos, G. E. (2011). Linear hybrid system falsification through local search. In Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA 2011), Taipei, Taiwan, October 11–14, 2011 (pp. 503–510). https://doi.org/10.1007/978-3-642-24372-1_39.

    Chapter  Google Scholar 

  2. Althoff, M., & Grebenyuk, D. (2016). Implementation of interval arithmetic in CORA 2016. In ARCH Workshop (pp. 91–105). Manchester: EasyChair.

    Google Scholar 

  3. Alur, R., Courcoubetis, C., Henzinger, T. A., & Ho, P. H. (1993). Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R. L. Grossman, A. Nerode, A. P. Ravn, & H. Rischel (Eds.), Hybrid systems. Lecture notes in computer science (Vol. 736, pp. 209–229). Berlin: Springer.

    Google Scholar 

  4. Angeli, D. (2002). A Lyapunov approach to incremental stability properties. IEEE Transactions on Automatic Control, 47(3), 410–421.

    Article  MathSciNet  Google Scholar 

  5. Annapureddy, Y., Liu, C., Fainekos, G., & Sankaranarayanan, S. (2011). S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In TACAS. Berlin: Springer.

    Google Scholar 

  6. Aréchiga, N., Kapinski, J., Deshmukh, J. V., Platzer, A., & Krogh, B. (2015). Numerically-aided deductive safety proof for a powertrain control system. Electronic Notes in Theoretical Computer Science, 317, 19–25.

    Article  MathSciNet  Google Scholar 

  7. Asarin, E., Bournez, O., Dang, T., & Maler, O. (2000). Approximate reachability analysis of piecewise-linear dynamical systems. In B. Krogh & N. Lynch (Eds.), Hybrid systems: computation and control. Lecture notes in computer science (Vol. 1790, pp. 20–31). Berlin: Springer.

    Google Scholar 

  8. Aylward, E.M., Parrilo, P.A., & Slotine, J. -J. E. (2008). Stability and robustness analysis of nonlinear systems via contraction metrics and SOS programming. Automatica, 44(8), 2163–2170.

    Article  MathSciNet  Google Scholar 

  9. Boichenko, V.A., & Leonov, G.A. (1998). Lyapunov’s direct method in estimates of topological entropy. Journal of Mathematical Sciences, 91(6), 3370–3379.

    Article  MathSciNet  Google Scholar 

  10. Boyd, S., El Ghaoui, L., Feron, E., & Balakrishnan, V. (1994). Linear matrix inequalities in system and control theory. Studies in applied mathematics (Vol. 15). Philadelphia, PA: SIAM.

    Book  Google Scholar 

  11. CAPD. (2002). Computer assisted proofs in dynamics.

    Google Scholar 

  12. Chan, N., & Mitra, S. (2017). Verified hybrid LQ control for autonomous spacecraft rendezvous. In 56th IEEE Annual Conference on Decision and Control, CDC 2017, Melbourne, December 12–15, 2017 (pp. 1427–1432). Piscataway: IEEE.

    Google Scholar 

  13. Chan, N., & Mitra, S. (2017) Verified hybrid LQ control for autonomous spacecraft rendezvous. In 2017 IEEE 56th Annual Conference on Decision and Control (CDC) (pp. 1427–1432). Piscataway: IEEE.

    Chapter  Google Scholar 

  14. Chan, N., & Mitra, S. (2017). Verifying safety of an autonomous spacecraft rendezvous mission. In ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, Collocated with Cyber-Physical Systems Week (CPSWeek), Pittsburgh, PA, April 17, 2017 (pp. 20–32).

    Google Scholar 

  15. Chen, X., Ábrahám, E., & Sankaranarayanan, S. (2013). Flow*: an analyzer for non-linear hybrid systems. In CAV (pp. 258–263). Berlin: Springer.

    Google Scholar 

  16. Cook, B. (2018). Formal reasoning about the security of amazon web services. In Computer Aided Verification—30th International Conference, CAV 2018, held as part of the Federated Logic Conference, FloC 2018, Oxford, July 14–17, 2018, Proceedings, Part I (pp. 38–47). New York: Springer International Publishing.

    Google Scholar 

  17. Dang, T., Le Guernic, C., & Maler, O. (2009). Computing reachable states for nonlinear biological models. In CMSB. Lecture notes in computer science (Vol. 5688, pp. 126–141). Berlin: Springer.

    Google Scholar 

  18. Donzé, A. (2010). Breach, a toolbox for verification and parameter synthesis of hybrid systems. In CAV (pp. 167–170). Berlin: Springer.

    Google Scholar 

  19. Donzé, A. (2010). Breach, a toolbox for verification and parameter synthesis of hybrid systems. In Computer Aided Verification. CAV 2010. Lecture Notes in Computer Science (Vol. 6174). Berlin: Springer.

    Chapter  Google Scholar 

  20. Donzé, A., & Maler, O. (2007). Systematic simulation using sensitivity analysis. In HSCC (pp. 174–189). Berlin: Springer.

    Google Scholar 

  21. Duggirala, P. S. (2015). Dynamic Analysis of Cyber-Physical Systems. PhD thesis. Champaign: University of Illinois at Urbana-Champaign.

    Google Scholar 

  22. Duggirala, P. S., Fan, C., Mitra, S., & Viswanathan, M. (2015). Meeting a powertrain verification challenge. In Computer Aided Verification (pp. 536–543). Berlin: Springer.

    Chapter  Google Scholar 

  23. Duggirala, P. S., Mitra, S., & Viswanathan, M. (2013). Verification of annotated models from executions. In EMSOFT (pp. 26:1–26:10). Piscataway: IEEE Press.

    Google Scholar 

  24. Duggirala, P. S., Mitra, S., Viswanathan, M., & Potok, M. (2015). C2E2: A verification tool for stateflow models. In TACAS (pp. 68–82). Berlin: Springer.

    Google Scholar 

  25. Duggirala, P. S., Wang, L., Mitra, S., Viswanathan, M., & Muñoz, C. (2014). Temporal precedence checking for switched models and its application to a parallel landing protocol. In Formal methods (pp. 215–229). Cham: Springer.

    Google Scholar 

  26. El-Guindy, A., Han, D., & Althoff, M. (2016) Formal analysis of drum-boiler units to maximize the load-following capabilities of power plants. IEEE Transactions on Power Systems (99), 1–12.

    Google Scholar 

  27. Fainekos, G. E. (2015). Automotive control design bug-finding with the s-taliro tool. In American Control Conference, ACC 2015, Chicago, IL, July 1–3, 2015 (p. 4096). Piscataway: IEEE.

    Google Scholar 

  28. Fainekos, G. E., Sankaranarayanan, S., Ueda, K., & Yazarel, H. (2012) Verification of automotive control applications using S-TaLiRo. In American Control Conference (ACC), 2012 (pp. 3567–3572). Citeseer. Piscataway: IEEE.

    Google Scholar 

  29. Fan, C., Kapinski, J., Jin, X., & Mitra, S. (2016). Locally optimal reach set over-approximation for nonlinear systems. In EMSOFT (pp. 6:1–6:10). New York: ACM.

    Google Scholar 

  30. Fan, C., & Mitra, S. (2015). Bounded verification with on-the-fly discrepancy computation. In ATVA (pp. 446–463). Berlin: Springer.

    Google Scholar 

  31. Fan, C., Qi, B., & Mitra, S. (2018). Data-driven formal reasoning and their applications in safety analysis of vehicle autonomy features. IEEE Design & Test, 35(3), 31–38.

    Article  Google Scholar 

  32. Fan, C., Qi, B., Mitra, S., Viswanathan, M. (2017). Dryvr: data-driven verification and compositional reasoning for automotive systems. In Computer Aided Verification, CAV 2017 (pp. 441–461). Heidelberg: Springer International Publishing

    Chapter  Google Scholar 

  33. Fan, C., Qi, B., Mitra, S., Viswanathan, M., & Duggirala, P. S. (2016). Automatic reachability analysis for nonlinear hybrid models with C2E2. In Computer Aided Verification–28th International Conference, CAV 2016, Toronto, ON, July 17–23, 2016, Proceedings, Part I (pp. 531–538). Cham: Springer.

    Google Scholar 

  34. Fränzle, M., Herde, C., Teige, T., Ratschan, S., & Schubert, T. (2007). Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT, 1(3–4), 209–236.

    MATH  Google Scholar 

  35. Frehse, G. (2005). Phaver: algorithmic verification of hybrid systems past hytech. In M. Morari & L.Thiele (Eds.), HSCC (Vol. 3414, pp. 258–273) Lecture notes in computer science . Berlin: Springer.

    Google Scholar 

  36. Frehse, G., Guernic, C. L., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T, & Maler, O. (2011). SpaceEx: scalable verification of hybrid systems. In S. Qadeer & G. Gopalakrishnan (Eds.), CAV. Lecture Notes in Computer Science. Berlin: Springer.

    Google Scholar 

  37. Girard, A., Pola, G., & Tabuada, P. (2010). Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Transactions on Automatic Control, 55(1), 116–126.

    Article  MathSciNet  Google Scholar 

  38. Henzinger, T. A. (1996). The theory of hybrid automata. In 11th Annual IEEE Symposium on Logic in Computer Science (pp. 278–292). Washington: IEEE Computer Society.

    Chapter  Google Scholar 

  39. Henzinger, T. A., Kopke, P. W., Puri, A., & Varaiya, P. (1998). What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57, 94–124.

    Article  MathSciNet  Google Scholar 

  40. Huang, Z., Fan, C., Mereacre, A., Mitra, S., & Kwiatkowska, M. Z. (2014). Invariant verification of nonlinear hybrid automata networks of cardiac cells. In CAV (pp. 373–390). Berlin: Springer.

    Google Scholar 

  41. Huang, Z., Fan, C., & Mitra, S. (2017). Bounded invariant verification for time-delayed nonlinear networked dynamical systems. Nonlinear Analysis: Hybrid Systems, 23, 211–229.

    MathSciNet  MATH  Google Scholar 

  42. Huang, Z., & Mitra, S. (2014). Proofs from simulations and modular annotations. In HSCC, Berlin, Germany. New York: ACM press.

    Google Scholar 

  43. Jewison, C., & Erwin, R. S. (2016). A spacecraft benchmark problem for hybrid control and estimation. In 2016 IEEE 55th Conference on Decision and Control (CDC) (pp. 3300–3305). Piscataway: IEEE.

    Chapter  Google Scholar 

  44. Jiang, Z., Pajic, M., Moarref, S., Alur, R., & Mangharam, R. (2012). Modeling and verification of a dual chamber implantable pacemaker. In TACAS (pp. 188–203). Berlin: Springer.

    Google Scholar 

  45. Jin, X., Deshmukh, J. V., Kapinski, J., Ueda, K., & Butts, K. (2014). Powertrain control verification benchmark. In Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC ’14 (pp. 253–262). New York, NY: ACM.

    MATH  Google Scholar 

  46. Jin, X., Deshmukh, J. V., Kapinski, J., Ueda, K., & Butts, K. R. (2014). Powertrain control verification benchmark. In 17th International Conference on Hybrid Systems: Computation and Control (Part of CPS Week), HSCC’14, Berlin, April 15–17, 2014 (pp. 253–262). New York: ACM.

    Google Scholar 

  47. Jin, X., Donzé, A., Deshmukh, J. V., & Seshia, S. A. (2015). Mining requirements from closed-loop control models. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 34(11), 1704–1717.

    Article  Google Scholar 

  48. Johnson, T. T., Green, J., Mitra, S., Dudley, R., & Erwin, R. S. (2012). Satellite rendezvous and conjunction avoidance: case studies in verification of nonlinear hybrid systems. In FM 2012: Formal Methods—18th International Symposium, Paris, France, August 27–31, 2012. Proceedings (pp. 252–266). Berlin: Springer.

    Google Scholar 

  49. Julius, A. A., & Pappas, G. J. (2009). Trajectory based verification using local finite-time invariance. In HSCC (pp. 223–236). Berlin: Springer.

    Google Scholar 

  50. Kapinski, J., Deshmukh, J. V., Jin, X., Ito, H., & Butts, K. (2016). Simulation-based approaches for verification of embedded control systems: an overview of traditional and advanced modeling, testing, and verification techniques. IEEE Control Systems, 36(6), 45–64.

    Article  MathSciNet  Google Scholar 

  51. Kaynar, D. K., Lynch, N., Segala, R., & Vaandrager, F. (2005). The theory of timed I/O automata. Synthesis Lectures on Computer Science. Morgan Claypool, November. Also available as Technical Report MIT-LCS-TR-917.

    Google Scholar 

  52. Kaynar, D. K., Lynch, N., Segala, R., & Vaandrager, F. (2010). The theory of timed I/O automata. Synthesis Lectures on Distributed Computing Theory, 1(1), 1–137.

    Article  Google Scholar 

  53. Kearns, M. J., & Vazirani, U. V. (1994) An introduction to computational learning theory. Cambridge: MIT press.

    Book  Google Scholar 

  54. Kong, S., Gao, S., Chen, W., & Clarke, E. (2015) dReach: δ-reachability analysis for hybrid systems. In TACAS (pp. 200–205). Berlin: Springer.

    Google Scholar 

  55. Koopman, P., & Wagner, M. (2016) Challenges in autonomous vehicle testing and validation. SAE International Journal of Transportation Safety, 4(2016-01-0128), 15–24.

    Google Scholar 

  56. Krstic, M., Kokotovic, P. V., & Kanellakopoulos, I. (1995). Nonlinear and adaptive control design (1st ed.). New York, NY: Wiley.

    MATH  Google Scholar 

  57. Liberzon, D. (2012). Switching in systems and control. Berlin: Springer Science & Business Media.

    MATH  Google Scholar 

  58. Lohmiller, W., & Slotine, J. -J. E. (1998) On contraction analysis for non-linear systems. Automatica, 34(6), 683–696.

    Article  MathSciNet  Google Scholar 

  59. Maidens, J., & Arcak, M. (2015). Reachability analysis of nonlinear systems using matrix measures. IEEE Transactions on Automatic Control, 60(1), 265–270.

    Article  MathSciNet  Google Scholar 

  60. Malladi, B. P., Sanfelice, R. G., Butcher, E., & Wang, J. (2016). Robust hybrid supervisory control for rendezvous and docking of a spacecraft. In 2016 IEEE 55th Conference on Decision and Control (CDC) (pp. 3325–3330). Piscataway: IEEE.

    Chapter  Google Scholar 

  61. Mitra, S. (September 2007). A Verification Framework for Hybrid Systems. PhD thesis. Cambridge, MA: Massachusetts Institute of Technology, 02139.

    Google Scholar 

  62. Nedialkov, N. (2006). VNODE-LP: validated solutions for initial value problem for ODEs. Technical report. Hamilton: McMaster University.

    Google Scholar 

  63. Perry, R. B., Madden, M. M., Torres-Pomales, W., & Butler, R. W. (2013). The simplified aircraft-based paired approach with the ALAS alerting algorithm. Technical Report NASA/TM-2013-217804. Hampton: NASA, Langley Research Center.

    Google Scholar 

  64. Road vehicles—Functional safety. (November 2011). Standard, International Organization for Standardization (ISO), Geneva, Switzerland.

    Google Scholar 

  65. Sankaranarayanan, S., Kumar, S. A., Cameron, F., Bequette, B. W., Fainekos, G., & Maahs, D. M. (March 2017) Model-based falsification of an artificial pancreas control system. SIGBED Review, 14(2), 24–33.

    Article  Google Scholar 

  66. Sontag, E. D. (2010). Contractive systems with inputs. In Perspectives in mathematical system theory, control, and signal processing (pp. 217–228). Berlin: Springer.

    Chapter  Google Scholar 

  67. Vladimerou, V., Prabhakar, P., Viswanathan, M., & Dullerud, G. E. (2008). Stormed hybrid systems. In ICALP (2). Lecture Notes in Computer Science (Vol. 5126, pp. 136–147). Berlin: Springer.

    Google Scholar 

  68. Zamani, M., Pola, G., Mazo, M., & Tabuada, P. (2012). Symbolic models for nonlinear control systems without stability assumptions. IEEE Transactions on Automatic Control, 57(7), 1804–1809.

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Illinois at Urbana-Champaign, ECE Department, Champaign, IL, USA

    Chuchu Fan & Sayan Mitra

Authors
  1. Chuchu Fan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sayan Mitra
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sayan Mitra .

Editor information

Editors and Affiliations

  1. University of California, Irvine, Irvine, CA, USA

    Mohammad Abdullah Al Faruque

  2. Siemens Corporate Technology, Princeton, NJ, USA

    Arquimedes Canedo

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Fan, C., Mitra, S. (2019). Data-Driven Safety Verification of Complex Cyber-Physical Systems. In: Al Faruque, M., Canedo, A. (eds) Design Automation of Cyber-Physical Systems. Springer, Cham. https://doi.org/10.1007/978-3-030-13050-3_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-13050-3_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-13049-7

  • Online ISBN: 978-3-030-13050-3

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation