Skip to main content
SpringerLink
Log in

Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10227))

Included in the following conference series:

Abstract

We propose a method for verifying persistence of nonlinear hybrid systems. Given some system and an initial set of states, the method can guarantee that system trajectories always eventually evolve into some specified target subset of the states of one of the discrete modes of the system, and always remain within this target region. The method also computes a time-bound within which the target region is always reached. The approach combines flow-pipe computation with deductive reasoning about invariants and is more general than each technique alone. We illustrate the method with a case study concerning showing that potentially destructive stick-slip oscillations of an oil-well drill eventually die away for a certain choice of drill control parameters. The case study demonstrates how just using flow-pipes or just reasoning about invariants alone can be insufficient. The case study also nicely shows the richness of systems that the method can handle: the case study features a mode with non-polynomial (nonlinear) ODEs and we manage to prove the persistence property with the aid of an automatic prover specifically designed for handling transcendental functions.

This material is based upon work supported by the UK Engineering and Physical Sciences Research Council under grants EPSRC EP/I010335/1 and EP/J001058/1, the National Science Foundation (NSF) under grant numbers CNS 1464311 and CCF 1527398, the Air Force Research Laboratory (AFRL) through contract number FA8750-15-1-0105, and the Air Force Office of Scientific Research (AFOSR) under contract number FA9550-15-1-0258.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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.

    Metric Temporal Logic; see e.g. [22].

  2. 2.

    The system exhibits sliding behaviour on a portion of this surface known as the sliding set. See [34].

  3. 3.

    Files for the case study are available online. http://www.verivital.com/nfm2017.

  4. 4.

    Here \(\nabla \) denotes the gradient of V, i.e. the vector of partial derivatives \((\frac{\partial V}{\partial x_1},\dots ,\frac{\partial V}{\partial x_n})\).

  5. 5.

    E.g. those featured in the right-hand side of the ODE, i.e. \(f({\varvec{x}})\).

  6. 6.

    Intel i5-2520M CPU @ 2.50 GHz, 4 GB RAM, running Arch Linux kernel 4.2.5-1.

  7. 7.

    E.g. numerical solution computation with “qualitative” features, such as invariance of certain regions.

References

  1. CAPD library. http://capd.ii.uj.edu.pl/

  2. Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175–205 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  3. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991–1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993). doi:10.1007/3-540-57318-6_30

    Chapter  Google Scholar 

  4. Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliab. Comput. 4(4), 361–369 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  5. Blanchini, F.: Set invariance in control. Automatica 35(11), 1747–1767 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  6. Carter, R.A.: Verification of liveness properties on hybrid dynamical systems. Ph.D. thesis, University of Manchester, School of Computer Science (2013)

    Google Scholar 

  7. Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_18

    Chapter  Google Scholar 

  8. Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14(4), 583–604 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  9. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975). doi:10.1007/3-540-07407-4_17

    Chapter  Google Scholar 

  10. Donzé, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 174–189. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71493-4_16

    Chapter  Google Scholar 

  11. Duggirala, P.S., Mitra, S.: Abstraction refinement for stability. In: Proceedings of 2011 IEEE/ACM International Conference on Cyber-Physical Systems, ICCPS, pp. 22–31, April 2011

    Google Scholar 

  12. Duggirala, P.S., Mitra, S.: Lyapunov abstractions for inevitability of hybrid systems. In: HSCC, pp. 115–124. ACM, New York (2012)

    Google Scholar 

  13. Eggers, A., Ramdani, N., Nedialkov, N.S., Fränzle, M.: Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods. Softw. Syst. Model. 14(1), 121–148 (2015)

    Article  MATH  Google Scholar 

  14. Frehse, G., Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_30

    Chapter  Google Scholar 

  15. Fulton, N., Mitsch, S., Quesel, J.-D., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527–538. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_36

    Chapter  Google Scholar 

  16. Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 279–294. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_19

    Chapter  Google Scholar 

  17. Ghorbal, K., Sogokon, A., Platzer, A.: A hierarchy of proof rules for checking differential invariance of algebraic sets. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 431–448. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46081-8_24

    Google Scholar 

  18. Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 190–203. Springer, Heidelberg (2008). doi:10.1007/978-3-540-70545-1_18

    Chapter  Google Scholar 

  19. Henzinger, T.A.: The Theory of Hybrid Automata, pp. 278–292. IEEE Computer Society Press, Washington, DC (1996)

    Google Scholar 

  20. Immler, F.: Verified reachability analysis of continuous systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 37–51. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_3

    Google Scholar 

  21. Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_15

    Google Scholar 

  22. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)

    Article  Google Scholar 

  23. Lin, Y., Stadtherr, M.A.: Validated solutions of initial value problems for parametric ODEs. Appl. Numer. Math. 57(10), 1145–1162 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  24. Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1–15. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17164-2_1

    Chapter  Google Scholar 

  25. Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT, pp. 97–106. ACM (2011)

    Google Scholar 

  26. Lygeros, J., Johansson, K.H., Simić, S.N., Zhang, J., Sastry, S.S.: Dynamical properties of hybrid automata. IEEE Trans. Autom. Control 48(1), 2–17 (2003)

    Article  MathSciNet  Google Scholar 

  27. Maidens, J.N., Arcak, M.: Reachability analysis of nonlinear systems using matrix measures. IEEE Trans. Autom. Control 60(1), 265–270 (2015)

    Article  MathSciNet  Google Scholar 

  28. Maidens, J.N., Arcak, M.: Trajectory-based reachability analysis of switched nonlinear systems using matrix measures. In: CDC, pp. 6358–6364, December 2014

    Google Scholar 

  29. Makino, K., Berz, M.: Cosy infinity version 9. Nucl. Instrum. Methods Phys. Res., Sect. A 558(1), 346–350 (2006)

    Article  Google Scholar 

  30. Matringe, N., Moura, A.V., Rebiha, R.: Generating invariants for non-linear hybrid systems by linear algebraic methods. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 373–389. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15769-1_23

    Chapter  Google Scholar 

  31. Mitrohin, C., Podelski, A.: Composing stability proofs for hybrid systems. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 286–300. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24310-3_20

    Chapter  Google Scholar 

  32. Möhlmann, E., Hagemann, W., Theel, O.: Hybrid tools for hybrid systems – proving stability and safety at once. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 222–239. Springer, Cham (2015). doi:10.1007/978-3-319-22975-1_15

    Chapter  Google Scholar 

  33. Möhlmann, E., Theel, O.: Stabhyli: a tool for automatic stability verification of non-linear hybrid systems. In: HSCC, pp. 107–112. ACM (2013)

    Google Scholar 

  34. Navarro-López, E.M., Carter, R.: Hybrid automata: an insight into the discrete abstraction of discontinuous systems. Int. J. Syst. Sci. 42(11), 1883–1898 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  35. Navarro-López, E.M., Carter, R.: Deadness and how to disprove liveness in hybrid dynamical systems. Theor. Comput. Sci. 642(C), 1–23 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  36. Navarro-López, E.M., Suárez, R.: Practical approach to modelling and controlling stick-slip oscillations in oilwell drillstrings. In: Proceedings of the 2004 IEEE International Conference on Control Applications, vol. 2, pp. 1454–1460. IEEE (2004)

    Google Scholar 

  37. Nedialkov, N.S.: Interval tools for ODEs and DAEs. In: SCAN (2006)

    Google Scholar 

  38. Neher, M., Jackson, K.R., Nedialkov, N.S.: On Taylor model based integration of ODEs. SIAM J. Numer. Anal. 45(1), 236–262 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  39. Nishida, T., Mizutani, K., Kubota, A., Doshita, S.: Automated phase portrait analysis by integrating qualitative and quantitative analysis. In: Proceedings of the 9th National Conference on Artificial Intelligence, pp. 811–816 (1991)

    Google Scholar 

  40. Paulson, L.C.: MetiTarski: past and future. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 1–10. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32347-8_1

    Chapter  Google Scholar 

  41. Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143–189 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  42. Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309–352 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  43. Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 176–189. Springer, Heidelberg (2008). doi:10.1007/978-3-540-70545-1_17

    Chapter  Google Scholar 

  44. Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008). doi:10.1007/978-3-540-71070-7_15

    Chapter  Google Scholar 

  45. Podelski, A., Wagner, S.: Model checking of hybrid systems: from reachability towards stability. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 507–521. Springer, Heidelberg (2006). doi:10.1007/11730637_38

    Chapter  Google Scholar 

  46. Podelski, A., Wagner, S.: Region stability proofs for hybrid systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 320–335. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75454-1_23

    Chapter  Google Scholar 

  47. Podelski, A., Wagner, S.: A sound and complete proof rule for region stability of hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 750–753. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71493-4_76

    Chapter  Google Scholar 

  48. Prabhakar, P., Garcia Soto, M.: Abstraction based model-checking of stability of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 280–295. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_20

    Chapter  Google Scholar 

  49. Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24743-2_32

    Chapter  Google Scholar 

  50. Ratschan, S., She, Z.: Providing a basin of attraction to a target region of polynomial systems by computation of Lyapunov-like functions. SIAM J. Control Optim. 48(7), 4377–4394 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  51. Richardson, D.: Some undecidable problems involving elementary functions of a real variable. J. Symb. Logic 33(4), 514–520 (1968)

    Article  MathSciNet  MATH  Google Scholar 

  52. Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed points. In: HSCC, pp. 221–230 (2010)

    Google Scholar 

  53. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. FMSD 32(1), 25–55 (2008)

    MATH  Google Scholar 

  54. Sogokon, A., Ghorbal, K., Jackson, P.B., Platzer, A.: A method for invariant generation for polynomial continuous systems. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 268–288. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49122-5_13

    Chapter  Google Scholar 

  55. Sogokon, A., Jackson, P.B.: Direct formal verification of liveness properties in continuous and hybrid dynamical systems. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 514–531. Springer, Cham (2015). doi:10.1007/978-3-319-19249-9_32

    Chapter  Google Scholar 

  56. Sogokon, A., Jackson, P.B., Johnson, T.T.: Verifying safety and persistence properties of hybrid systems using flowpipes and continuous invariants. Technical report, Vanderbilt University (2017)

    Google Scholar 

  57. Strzeboński, A.W.: Cylindrical decomposition for systems transcendental in the first variable. J. Symb. Comput. 46(11), 1284–1290 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  58. Taly, A., Tiwari, A.: Deductive verification of continuous dynamical systems. In: Kannan, R., Kumar, K.N. (eds.) FSTTCS. LIPIcs, vol. 4, pp. 383–394. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Wadern (2009)

    Google Scholar 

  59. Tiwari, A.: Generating box invariants. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 658–661. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78929-1_58

    Chapter  Google Scholar 

  60. Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382–399. Springer, Cham (2015). doi:10.1007/978-3-319-25423-4_25

    Chapter  Google Scholar 

  61. Xue, B., Easwaran, A., Cho, N.J., Fränzle, M.: Reach-avoid verification for nonlinear systems based on boundary analysis. IEEE Trans. Autom. Control (2016)

    Google Scholar 

  62. Zhao, H., Yang, M., Zhan, N., Gu, B., Zou, L., Chen, Y.: Formal verification of a descent guidance control program of a lunar lander. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 733–748. Springer, Cham (2014). doi:10.1007/978-3-319-06410-9_49

    Chapter  Google Scholar 

  63. Zhao, H., Zhan, N., Kapur, D.: Synthesizing switching controllers for hybrid systems by generating invariants. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 354–373. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39698-4_22

    Chapter  Google Scholar 

Download references

Acknowledgements

The authors wish to thank to the anonymous reviewers for their careful reading and valuable suggestions for improving this paper.

Author information

Authors and Affiliations

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

    Andrew Sogokon & Taylor T. Johnson

  2. Laboratory for Foundations of Computer Science, University of Edinburgh, Edinburgh, Scotland, UK

    Paul B. Jackson

Authors
  1. Andrew Sogokon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paul B. Jackson
    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 Andrew Sogokon .

Editor information

Editors and Affiliations

  1. Stanford University, Palo Alto, California, USA

    Clark Barrett

  2. NASA Ames Research Center, Moffett Field, California, USA

    Misty Davies

  3. NASA Ames Research Center, Moffett Field, California, USA

    Temesghen Kahsai

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Sogokon, A., Jackson, P.B., Johnson, T.T. (2017). Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants. In: Barrett, C., Davies, M., Kahsai, T. (eds) NASA Formal Methods. NFM 2017. Lecture Notes in Computer Science(), vol 10227. Springer, Cham. https://doi.org/10.1007/978-3-319-57288-8_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-57288-8_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-57287-1

  • Online ISBN: 978-3-319-57288-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation