Advertisement

Combining Formal and Informal Methods in the Design of Spacecrafts

  • Mengfei Yang
  • Naijun ZhanEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9506)

Abstract

In this chapter, we summarize our experience on combing formal and informal methods together in the design of spacecrafts. With our approach, the designer can either build an executable model of a spacecraft using the industrial standard environment Simulink/Stateflow, which facilitates analysis by simulation, or construct a formal model using Hybrid CSP (HCSP), which is an extension of CSP for formally modeling hybrid systems. HCSP processes can be specified and reasoned about by Hybrid Hoare Logic (HHL), which is an extension of Hoare logic to hybrid systems. The connection between informal and formal methods is realized via an automatic translator from Simulink/Stateflow diagrams to HCSP and an inverse translator from HCSP to Simulink. The advantages of combining formal and informal methods in the design of spacecrafts include
  • It enables formal verification as a complementation of simulation. As the inherent incompleteness of simulation, it has become an agreement in industry and academia to complement simulation with formal verification, but this issue still remains challenging although lots of attempts have been done (see the related work section);

  • It provides an option to start the design of a hybrid system with an HCSP formal model, and simulate and/or test it using Matlab platform economically, without expensive formal verification if not necessary;

  • The semantic preservation in shifting between formal and informal models is justified by co-simulation. Therefore, it provides the designer the flexibility using formal and informal methods according to the trade-off between efficiency and cost, and correctness and reliability.

We will demonstrate the above approach by analysis and verification of the descent guidance control program of a lunar lander, which is a real-world industry example.

Keywords

Spacecraft Lunar lander Simulink/Stateflow formal methods hybrid systems 

Notes

Acknowledgements

We thank all of our collaborators with whom the joint work are reported in this chapter, including Prof. Chaochen Zhou, Prof. Martin Fränzle, Prof. Shengchao Qin, Prof. Anders P. Ravn, Prof. Tao Tang, Prof. Bin Gu, Dr. Jiang Liu, Dr. Jidong Lv, Dr. Shuling Wang, Dr. Hengjun Zhao, Dr. Liang Zou, Dr. Yao Chen, Mr. Mingshuai Chen and Mr. Zhao Quan.

References

  1. 1.
  2. 2.
  3. 3.
    SysML V 1.4 Beta Specification (2013). http://www.omg.org/spec/SysML
  4. 4.
    Eggers, A., Fränzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171–185. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  5. 5.
    Agrawal, A., Simon, G., Karsai, G.: Semantic translation of simulink/stateflow models to hybrid automata using graph transformations. Int. Workshop Graph Transform. Visual Model. Tech. 109, 43–56 (2004)zbMATHGoogle Scholar
  6. 6.
    Alur, R., Henzinger, T.A.: Modularity for timed and hybrid systems. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243. Springer, Heidelberg (1997)Google Scholar
  7. 7.
    Anta, A., Majumdar, R., Saha, I., Tabuada, P.: Automatic verification of control system implementations. In: EMSOFT 2010, pp. 9–18 (2010)Google Scholar
  8. 8.
    Asarin, E., Dang, T., Maler, O.: The \(\mathbf{d/dt}\) tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365–370. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  9. 9.
    Balarin, F., Watanabe, Y., Hsieh, H., Lavagno, L., Passerone, C., Sangiovanni-Vincentelli, A.L.: Metropolis: an integrated electronic system design environment. IEEE Comput. 36(4), 45–52 (2003)CrossRefGoogle Scholar
  10. 10.
    Bouissou, O., Goubault, E., Putot, S., Tekkal, K., Vedrine, F.: HybridFluctuat: a static analyzer of numerical programs within a continuous environment. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 620–626. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  11. 11.
    Cavalcanti, A., Clayton, P., O’Halloran, C.: Control law diagrams in circus. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 253–268. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Chen, C., Dong, J.S., Sun, J.: A formal framework for modeling and validating simulink diagrams. Formal Asp. Comput. 21(5), 451–483 (2009)CrossRefzbMATHGoogle Scholar
  13. 13.
    Chen, M., Han, X., Tang, T., Wang, S., Yang, M., Zhan, N., Zhao, H., Zou, L.: MARS: A toolchain for modeling, analysis and verification of spacecraft control systems. Technical Report ISCAS-SKLCS-15-04, State Key Laboratories of Computer Science, Institute of Software, CAS (2015)Google Scholar
  14. 14.
    Chen, M., Ravn, A., Yang, M., Zhan, N., Zou, L.: A two-way path between formal and informal design of embedded systems. Technical Report ISCAS-SKLCS-15-06, State Key Laboratories of Computer Science, Institute of Software, Chinese Academy of Sciences (2015)Google Scholar
  15. 15.
    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)CrossRefGoogle Scholar
  16. 16.
    Cousot, P.: Integrating physical systems in the static analysis of embedded control software. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 135–138. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  17. 17.
    Deng, Y., Rajhans, A., Julius, A.A.: STRONG: a trajectory-based verification toolbox for hybrid systems. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 165–168. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  18. 18.
    Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  19. 19.
    Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68–82. Springer, Heidelberg (2015)Google Scholar
  20. 20.
    Eker, J., Janneck, J., Lee, E.A., Liu, J., Liu, X., Ludvig, J., Neuendorffer, S., Sachs, S., Xiong, Y.: Taming heterogeneity - the ptolemy approach. Proc. IEEE 91(1), 127–144 (2003)CrossRefGoogle Scholar
  21. 21.
    Esteve, M.-A., Katoen, J.-P., Nguyen, V., Postma, B., Yushtein, Y.: Formal correctness, safety, dependability, and performance analysis of a satellite. In: ICSE 2012, pp. 1022–1031 (2012)Google Scholar
  22. 22.
    Goubault, E., Martel, M., Putot, S.: Some future challenges in the validation of control systems. In: ERTS 2006 (2006)Google Scholar
  23. 23.
    Hamon, G., Rushby, J.: An operational semantics for stateflow. Int. J. Softw. Tools Technol. Transf. 9(5), 447–456 (2007)CrossRefzbMATHGoogle Scholar
  24. 24.
    He, J.: From CSP to hybrid systems. In: Roscoe, A.W. (ed.) A Classical Mind, Essays in Honour of C.A.R. Hoare, pp. 171–189. Prentice Hall International (UK) Ltd, Hertfordshire (1994)Google Scholar
  25. 25.
    Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996, pp. 278–292, July 1996Google Scholar
  26. 26.
    Hoare, C.A.R., He, J.: Unifying Theories of Programming, vol. 14. Prentice Hall, Englewood Cliffs (1998)zbMATHGoogle Scholar
  27. 27.
    Johnson, T.T., Green, J., Mitra, S., Dudley, R., Erwin, R.S.: Satellite rendezvous and conjunction avoidance: case studies in verification of nonlinear hybrid systems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 252–266. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  28. 28.
    Kong, H., He, F., Song, X., Hung, W.N.N., Gu, M.: Exponential-condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 242–257. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  29. 29.
    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)CrossRefGoogle Scholar
  30. 30.
    Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT 2011, pp. 97–106 (2011)Google Scholar
  31. 31.
    Liu, J., Zhan, N., Zhao, H.: Automatically discovering relaxed lyapunov functions for polynomial dynamical systems. Math. Comput. Sci. 6(4), 395–408 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Liu, J., Zhan, N., Zhao, H., Zou, L.: Abstraction of elementary hybrid systems by variable transformation. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 360–377. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  33. 33.
    Majumdar, R., Saha, I., Shashidhar, K.C., Wang, Z.: CLSE: closed-loop symbolic execution. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 356–370. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  34. 34.
    Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating simulink models into input language of a model checker. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606–620. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  35. 35.
    Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58–64 (2010)CrossRefGoogle Scholar
  36. 36.
    Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41(2), 143–189 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  37. 37.
    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)CrossRefGoogle Scholar
  38. 38.
    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)CrossRefGoogle Scholar
  39. 39.
    Scaife, N., Sofronis, C., Caspi, P., Tripakis, S., Maraninchi, F.: Defining and translating a safe subset of simulink/stateflow into lustre. In: EMSOFT 2004, pp. 259–268. ACM (2004)Google Scholar
  40. 40.
    Selic, B., Gerard, S.: Modeling and Analysis or Real-Time and Embedded Systems with UML and MARTE: Developing Cyber-Physical Systems. The MK/OMG Press, Burlington (2013)Google Scholar
  41. 41.
    Tiller, M.: Introduction to Physical Modeling with Modelica, vol. 615. Springer, New York (2001)CrossRefGoogle Scholar
  42. 42.
    Tiwari, A.: Formal semantics and analysis methods for Simulink Stateflow models. Technical report, SRI International, (2002)Google Scholar
  43. 43.
    Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Embed. Comput. Syst. 4(4), 779–818 (2005)CrossRefGoogle Scholar
  44. 44.
    Wang, S., Zhan, N., Guelev, D.: An assume/guarantee based compositional calculus for hybrid CSP. In: Agrawal, M., Cooper, S.B., Li, A. (eds.) TAMC 2012. LNCS, vol. 7287, pp. 72–83. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  45. 45.
    Wang, S., Zhan, N., Zou, L.: An improved hhl prover: an interactive theorem prover for hybrid systems. In: Butler, M., et al. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382–399. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-25423-4_25 CrossRefGoogle Scholar
  46. 46.
    Zhan, N., Wang, S., Guelev, D.: Extending Hoare logic to hybrid systems. Technical report ISCAS-SKLCS-13-02, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (2013)Google Scholar
  47. 47.
    Zhan, N., Wang, S., Zhao, H.: Formal modelling, analysis and verification of hybrid systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Unifying Theories of Programming and Formal Engineering Methods. LNCS, vol. 8050, pp. 207–281. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  48. 48.
    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, Heidelberg (2014)CrossRefGoogle Scholar
  49. 49.
    Zhou, C., Hansen, M.R.: Duration Calculus – A Formal Approach to Real-Time Systems. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  50. 50.
    Zhou, C., Hoare, C.A.R., Ravn, A.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  51. 51.
    Chaochen, Z., Ji, W., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  52. 52.
    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. LNCS, vol. 8164, pp. 262–280. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  53. 53.
    Zou, L., Zhan, N., Wang, S., Fränzle, M.: Formal verification of simulink/stateflow diagrams. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 464–481. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-24953-7_33 CrossRefGoogle Scholar
  54. 54.
    Zou, L., Zhan, N., Wang, S., Fränzle, M., Qin, S.: Verifying Simulink diagrams via a hybrid hoare logic prover. In: EMSOFT 2013, pp. 1–10 (2013)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Chinese Academy of Space TechnologyBeijingChina
  2. 2.State Key Laboratory of Computer ScienceInstitute of Software, CASBeijingChina

Personalised recommendations