Advertisement

MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems

  • Mingshuai ChenEmail author
  • Xiao Han
  • Tao Tang
  • Shuling Wang
  • Mengfei Yang
  • Naijun Zhan
  • Hengjun Zhao
  • Liang Zou
Chapter
Part of the NASA Monographs in Systems and Software Engineering book series (NASA)

Abstract

We introduce a toolchain MARS for Modelling, Analyzing and veRifying hybrid Systems we developed in the past years. Using MARS, we build executable models of hybrid systems using the industrial standard environment Simulink/Stateflow, which facilitates analysis by simulation. To complement simulation, formal verification of Simulink/Stateflow models is conducted in the toolchain via the following steps: first, we translate Simulink/Stateflow diagrams to Hybrid CSP (HCSP) processes by an automatic translator Sim2HCSP, where HCSP is an extension of CSP for formally modelling hybrid systems; second, to justify the translation, another automatic translator HCSP2Sim that translates from HCSP to Simulink is provided, so that the consistency between the original Simulink/Stateflow model and the translated HCSP formal model can be checked by co-simulation; then, the HCSP processes obtained in the first step are verified by an interactive Hybrid Hoare Logic (HHL) prover; during the verification, an invariant generator independent of the theorem prover for synthesizing invariants for differential equations and loops is needed. We will demonstrate the toolchain by analysis and verification of a descent guidance control program of a lunar lander, which is a real-world industry example.

Keywords

Hybrid System Invariant Generator Hybrid Automaton Bound Model Check Quantifier Elimination 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Notes

Acknowledgements

The work is supported partly by “973 Program” under grant No. 2014CB340701, by NSFC under grants 91418204 and 91118007, by CDZ project CAP (GZ 1023), and by the CAS/SAFEA International Partnership Program for Creative Research Teams.

References

  1. 1.
    Aerts, A., Mousavi, M.R., Reniers, M.: A tool prototype for model-based testing of cyber-physical systems. In: Leucker, M., Rueda, C., Valencia, D.F. (eds.) ICTAC 2015, pp. 563–572. Springer International Publishing (2015)Google Scholar
  2. 2.
    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.) Hybrid Systems. Lecture Notes in Computer Science, vol. 736, pp. 209–229. Springer, Berlin, Heidelberg (1993)Google Scholar
  3. 3.
    Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011, pp. 254–257. Springer, Berlin, Heidelberg (2011)Google Scholar
  4. 4.
    Asarin, E., Dang, T., Maler, O.: The d/dt tool for verification of hybrid systems. In: CAV 2002. Lecture Notes in Computer Science, vol. 2404, pp. 365–370 (2002)Google Scholar
  5. 5.
    Chen, C., Dong, J.S., Sun, J.: A formal framework for modelling and validating Simulink diagrams. Form. Asp. Comput. 21(5), 451–483 (2009)Google Scholar
  6. 6.
    Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow\(^*\): An analyzer for non-linear hybrid systems. In: CAV 2013. Lecture Notes in Computer Science, vol. 8044, pp. 258–263 (2013)Google Scholar
  7. 7.
    Chen, M., Ravn, A., Yang, M., Zhan, N., Zou, L.: A two-way path between formal and informal design of embedded systems. In: Proc. UTP 2016 (2016)Google Scholar
  8. 8.
    Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. Lecture Notes in Computer Science, vol. 33, pp. 134–183. Springer, Berlin, Heidelberg (1975)Google Scholar
  9. 9.
    Dang, T., Nahhal, T.: Coverage-guided test generation for continuous and hybrid systems. Form. Methods Syst. Des. 34(2), 183–213 (2009)Google Scholar
  10. 10.
    Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1–2), 29–35 (1988)Google Scholar
  11. 11.
    De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS 2008. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer, Berlin, Heidelberg (2008)Google Scholar
  12. 12.
    Deng, Y., Rajhans, A., Julius, A.A.: STRONG: a trajectory-based verification toolbox for hybrid systems. In: QEST 2013. Lecture Notes in Computer Science, vol. 8054, pp. 165–168 (2013)Google Scholar
  13. 13.
    Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: CAV 2010. Lecture Notes in Computer Science, vol. 6174, pp. 167–170 (2010)Google Scholar
  14. 14.
    Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for annotated Stateflow models. In: TACAS 2015. Lecture Notes in Computer Science, vol. 9035, pp. 68–82 (2015)Google Scholar
  15. 15.
    Eggers, A., Ramdani, N., Nedialkov, N., Fränzle, M.: Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods. In: SEFM 2011, pp. 172–187. Springer-Verlag, Berlin, Heidelberg (2011)Google Scholar
  16. 16.
    Fulton, N., Mitsch, S., Quesel, J., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. CADE 2015, 527–538 (2015)Google Scholar
  17. 17.
    He, J.: From CSP to hybrid systems. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, pp. 171–189. Prentice Hall International (UK) Ltd. (1994)Google Scholar
  18. 18.
    Hoare, C.: Communicating Sequential Processes, vol. 178. Prentice-hall Englewood Cliffs (1985)Google Scholar
  19. 19.
    Kong, H., He, F., Song, X., Hung, W.N., Gu, M.: Exponential-condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. Lecture Notes in Computer Science, vol. 8044, pp. 242–257. Springer, Berlin Heidelberg (2013)Google Scholar
  20. 20.
    Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput 32(3), 231–253 (2001)Google Scholar
  21. 21.
    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. Lecture Notes in Computer Science, vol. 6461, pp. 1–15. Springer, Berlin, Heidelberg (2010)Google Scholar
  22. 22.
    Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT 2011, pp. 97–106. ACM, New York, NY, USA (2011)Google Scholar
  23. 23.
    Liu, J., Zhan, N., Zhao, H., Zou, L.: Abstraction of elementary hybrid systems by variable transformation. In: FM 2015. Lecture Notes in Computer Science, vol. 9109, pp. 360–377 (2015)Google Scholar
  24. 24.
    Löfberg, J.: YALMIP: a toolbox for modeling and optimization in MATLAB. In: Proceedings of the CACSD Conference. Taipei, Taiwan (2004). http://users.isy.liu.se/johanl/yalmip
  25. 25.
    Löfberg, J.: Pre- and post-processing sum-of-squares programs in practice. IEEE Trans. Autom. Control 54(5), 1007–1011 (2009)Google Scholar
  26. 26.
    Manna, Z., Pnueli, A.: Verifying hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems. Lecture Notes in Computer Science, vol. 736, pp. 4–35. Springer, Berlin, Heidelberg (1993)Google Scholar
  27. 27.
    Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)Google Scholar
  28. 28.
    Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Logic Comput. 20(1), 309–352 (2010)Google Scholar
  29. 29.
    Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Gupta, A., Malik, S. (eds.) CAV 2008. Lecture Notes in Computer Science, vol. 5123, pp. 176–189. Springer, Berlin, Heidelberg (2008)Google Scholar
  30. 30.
    Platzer, A., Quesel, J.D.: KeYmaera: a hybrid theorem prover for hybrid systems. In: IJCAR 2008. Lecture Notes in Computer Science, vol. 5195, pp. 171–178. Springer, Berlin, Heidelberg (2008)Google Scholar
  31. 31.
  32. 32.
    Toh, K.C., Todd, M., Tütüncü, R.H.: SDPT3 – a MATLAB software package for semidefinite programming. Optim. Methods Softw. 11, 545–581 (1999)Google Scholar
  33. 33.
    Tütüncü, R.H., Toh, K.C., Todd, M.J.: Solving semidefinite-quadratic-linear programs using SDPT3. Math. Program. 95(2), 189–217 (2003)Google Scholar
  34. 34.
    Vandenberghe, L., Boyd, S.: Semidefinite programming. SIAM Rev. 38(1), 49–95 (1996)Google Scholar
  35. 35.
    Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: ICFEM 2015. Lecture Notes in Computer Science, vol. 9407, pp. 382–399 (2015)Google Scholar
  36. 36.
    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: FM 2014. Lecture Notes in Computer Science, vol. 8442, pp. 733–748 (2014)Google Scholar
  37. 37.
    Zhou, C., Hansen, M.R.: Duration Calculus – A Formal Approach to Real-Time Systems. Monographs in Theoretical Computer Science. An EATCS Series. Springer-Verlag, Berlin Heidelberg (2004)Google Scholar
  38. 38.
    Zhou, C., Hoare, C., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)Google Scholar
  39. 39.
    Zhou, C., Wang, J., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) Hybrid Systems III. Lecture Notes in Computer Science, vol. 1066, pp. 511–530. Springer, Berlin, Heidelberg (1996)Google Scholar
  40. 40.
    Zou, L., Zhan, N., Wang, S., Fränzle, M., Qin, S.: Verifying Simulink diagrams via a Hybrid Hoare Logic prover. EMSOFT 2013, 1–10 (2013)Google Scholar
  41. 41.
    Zou, L., Lv, J., Wang, S., Zhan, N., Tang, T., Yuan, L., Liu, Y.: Verifying Chinese train control system under a combined scenario by theorem proving. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. Lecture Notes in Computer Science, vol. 8164, pp. 262–280. Springer, Berlin Heidelberg (2014)Google Scholar
  42. 42.
    Zou, L., Zhan, N., Wang, S., Fränzle, M.: Formal verification of Simulink/Stateflow diagrams. In: ATVA 2015. Lecture Notes in Computer Science, vol. 9346, pp. 464–481 (2015)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Mingshuai Chen
    • 1
    Email author
  • Xiao Han
    • 2
  • Tao Tang
    • 2
  • Shuling Wang
    • 1
  • Mengfei Yang
    • 3
  • Naijun Zhan
    • 1
  • Hengjun Zhao
    • 4
  • Liang Zou
    • 1
  1. 1.State Key Lab. of Computer ScienceInstitute of Software, Chinese Academy of SciencesBeijingPeople’s Republic of China
  2. 2.State Key Lab. of Rail Traffic Control and SafetyBeijing Jiaotong UniversityBeijingPeople’s Republic of China
  3. 3.Chinese Academy of Space TechnologyBeijingPeople’s Republic of China
  4. 4.School of Computer and Information ScienceSouthwest UniversityChongqingPeople’s Republic of China

Personalised recommendations