Skip to main content
SpringerLink
Log in

Combining Formal and Informal Methods in the Design of Spacecrafts

  • Conference paper
  • First Online:
Engineering Trustworthy Software Systems

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

This work is supported partly by “973 Program” under grant No. 2014CB340701, by NSFC under grants 91118007 and 91418204, and by the CAS/SAFEA International Partnership Program for Creative Research Teams.

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.

    Specific impulse is a physical quantity describing the efficiency of rocket engines. It equals the thrust produced per unit mass of propellant burned per second.

  2. 2.

    Note that if no shutdown signal is received, there exists possibility that the lander stays in the slow descent phase after landing.

  3. 3.

    We have abstracted away the domain constraints on \(F_c\).

  4. 4.

    http://www-polsys.lip6.fr/safey/RAGLib/.

References

  1. Simulink User’s Guide (2013). http://www.mathworks.com/help/pdf_doc/simulink/sl_using.pdf

  2. Stateflow User’s Guide (2013). http://www.mathworks.com/help/pdf_doc/stateflow/sf_using.pdf

  3. SysML V 1.4 Beta Specification (2013). http://www.omg.org/spec/SysML

  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)

    Chapter  Google Scholar 

  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)

    MATH  Google Scholar 

  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. Anta, A., Majumdar, R., Saha, I., Tabuada, P.: Automatic verification of control system implementations. In: EMSOFT 2010, pp. 9–18 (2010)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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. 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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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)

    Article  Google Scholar 

  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. Goubault, E., Martel, M., Putot, S.: Some future challenges in the validation of control systems. In: ERTS 2006 (2006)

    Google Scholar 

  23. Hamon, G., Rushby, J.: An operational semantics for stateflow. Int. J. Softw. Tools Technol. Transf. 9(5), 447–456 (2007)

    Article  MATH  Google Scholar 

  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. Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996, pp. 278–292, July 1996

    Google Scholar 

  26. Hoare, C.A.R., He, J.: Unifying Theories of Programming, vol. 14. Prentice Hall, Englewood Cliffs (1998)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Liu, J., Zhan, N., Zhao, H.: Automatically discovering relaxed lyapunov functions for polynomial dynamical systems. Math. Comput. Sci. 6(4), 395–408 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  35. Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58–64 (2010)

    Article  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. Tiller, M.: Introduction to Physical Modeling with Modelica, vol. 615. Springer, New York (2001)

    Book  Google Scholar 

  42. Tiwari, A.: Formal semantics and analysis methods for Simulink Stateflow models. Technical report, SRI International, (2002)

    Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    MATH  Google Scholar 

  50. Zhou, C., Hoare, C.A.R., Ravn, A.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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 

Download references

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.

Author information

Authors and Affiliations

  1. Chinese Academy of Space Technology, Beijing, China

    Mengfei Yang

  2. State Key Laboratory of Computer Science, Institute of Software, CAS, Beijing, China

    Naijun Zhan

Authors
  1. Mengfei Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Naijun Zhan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Naijun Zhan .

Editor information

Editors and Affiliations

  1. Southwest University, Chongqing, China

    Zhiming Liu

  2. Southwest University, Chongqing, China

    Zili Zhang

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Yang, M., Zhan, N. (2016). Combining Formal and Informal Methods in the Design of Spacecrafts. In: Liu, Z., Zhang, Z. (eds) Engineering Trustworthy Software Systems. Lecture Notes in Computer Science(), vol 9506. Springer, Cham. https://doi.org/10.1007/978-3-319-29628-9_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-29628-9_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-29627-2

  • Online ISBN: 978-3-319-29628-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation