Skip to main content
SpringerLink
Log in
SpringerLink
Log in

A Two-Way Path Between Formal and Informal Design of Embedded Systems

  • Conference paper
  • First Online:
Unifying Theories of Programming (UTP 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10134))

Included in the following conference series:

Abstract

It is well known that informal simulation-based design of embedded systems has a low initial cost and delivers early results; yet it cannot guarantee the correctness and reliability of the system to be developed. In contrast, the correctness and reliability of the system can be thoroughly investigated with formal design, but it requires a larger effort, which increases the development cost. Therefore, it is desirable for a designer to move between formal and informal design. This paper describes how to translate Hybrid CSP (HCSP) formal models into Simulink graphical models, so that the models can be simulated and tested using a MATLAB platform, thus avoiding expensive formal verification if the development is at a stage where it is considered unnecessary. Together with our previous work on encoding Simulink/Stateflow diagrams into HCSP, it provides a two-way path in the design of embedded systems, so that the designer can flexibly shift between formal and informal models. The translation from HCSP into Simulink diagrams is implemented as a fully automatic tool, and the correctness of the translation is justified using Unifying Theories of Programming (UTP).

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.

    An oracle that interprets non-determinism is none of the blocks in Simulink library, inasmuch as the random block provided by Simulink generates pseudo random numbers, which is in itself deterministic.

  2. 2.

    We always assume time evolution is modeled in \(S_C\), i.e., it contains \(\dot{now}=1\).

References

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

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

  3. Tiller, M.: Introduction to Physical Modeling with Modelica. Springer, New York (2001)

    Book  Google Scholar 

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

  5. Selic, B., Gerard, S.: Modeling and Analysis or Real-Time and Embedded Systems with UML and MARTE: Developing Cyber-Physical Systems. The Springer International Series in Engineering and Computer Science. The MK/OMG Press, Burlington (2013)

    Google Scholar 

  6. Balarin, F., Watanabe, Y., Hsieh, H., Lavagno, H., Passerone, C., Sangiovanni-Vincentelli, A.L.: Metropolis: an integrated electronic system design environment. IEEE Comput. 36(4), 45–52 (2003)

    Article  Google Scholar 

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

  8. Henzinger, T.: The theory of hybrid automata. In: LICS 1996, pp. 278–292, July 1996

    Google Scholar 

  9. Alur, R., Henzinger, T.A.: Modularity for timed and hybrid systems. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 74–88. Springer, Berlin (1997). doi:10.1007/3-540-63141-0_6

    Chapter  Google Scholar 

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

  11. Chaochen, Z., Ji, W., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 511–530. Springer, Berlin (1996). doi:10.1007/BFb0020972

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  13. 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, Berlin (2010). doi:10.1007/978-3-642-17164-2_1

    Chapter  Google Scholar 

  14. Zou, L., Zhan, N., Wang, V., Fränzle, M., Qin, S.: Verifying simulink diagrams via a hybrid hoare logic prover. In: EMSOFT 2013, pp. 1–10 (2013)

    Google Scholar 

  15. 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, Cham (2015). doi:10.1007/978-3-319-24953-7_33

    Chapter  Google Scholar 

  16. Chen, M., Ravn, A.P., Wang, S., Yang, M., Zhan, N.: A two-way path between formal and informal design of embedded systems (extended version). http://lcs.ios.ac.cn/~chenms/papers/UTP2016_FULL.pdf

  17. Simulink Design Verifier User’s Guide (2010). http://www.manualslib.com/manual/392930/Matlab-Simulink-Design-Verifier-1.html#manual

  18. Han, Z., Mosterman, P.J.: Towards sensitivity analysis of hybrid systems using simulink. HSCC 2013, 95–100 (2013)

    Article  MathSciNet  Google Scholar 

  19. Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time simulink to lustre. ACM Trans. Embedded Comput. Syst. 4(4), 779–818 (2005)

    Article  Google Scholar 

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

  21. Cavalcanti, A., Clayton, P., O’Halloran, C.: Control law diagrams in Circus. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 253–268. Springer, Berlin (2005). doi:10.1007/11526841_18

    Chapter  Google Scholar 

  22. Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Berlin (2002). doi:10.1007/3-540-45648-1_10

    Chapter  Google Scholar 

  23. Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating simulink models into input language of a model checker. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606–620. Springer, Berlin (2006). doi:10.1007/11901433_33

    Chapter  Google Scholar 

  24. Sfyrla, V., Tsiligiannis, G., Safaka, I., Bozga, M., Sifakis, J.: Compositional translation of simulink models into synchronous BIP. In: IEEE Fifth International Symposium on Industrial Embedded Systems, SIES 2010, pp. 217–220. IEEE (2010)

    Google Scholar 

  25. Bliudze, S., Sifakis, J.: The algebra of connectors - structuring interaction in BIP. IEEE Trans. Comput. 57(10), 1315–1330 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  26. Yang, C., Vyatkin, V.: Transformation of simulink models to IEC 61499 Function Blocks for verification of distributed control systems. Control Eng. Pract. 20(12), 1259–1269 (2012)

    Article  Google Scholar 

  27. Zhou, C., Kumar, R.: Semantic translation of simulink diagrams to input/output extended finite automata. Discrete Event Dyn. Syst. 22(2), 223–247 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  28. Minpoli, S., Frehse, G.: SL2SX translator: from simulink to SpaceEx verification tool. In: HSCC 2016 (2016)

    Google Scholar 

  29. Chen, R., 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 

  30. Boström, P.: Contract-based verification of simulink models. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 291–306. Springer, Berlin (2011). doi:10.1007/978-3-642-24559-6_21

    Chapter  Google Scholar 

  31. Roy, P., Shankar, N.: Simcheck: a contract type system for simulink. ISSE 7(2), 73–83 (2011)

    Google Scholar 

  32. Preoteasa, V., Tripakis, S.: Refinement calculus of reactive systems. In: EMSOFT 2014, pp. 2:1–2:10 (2014)

    Google Scholar 

  33. Dragomir, I., Preoteasa, V., Tripakis, S.: Compositional semantics and analysis of hierarchical block diagrams. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 38–56. Springer, Cham (2016). doi:10.1007/978-3-319-32582-8_3

    Chapter  Google Scholar 

  34. 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, Berlin (2013). doi:10.1007/978-3-642-39721-9_5

    Chapter  Google Scholar 

  35. 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, Berlin (2012). doi:10.1007/978-3-642-29952-0_13

    Chapter  Google Scholar 

  36. Guelev, D., Wang, S., Zhan, N.: Hoare reasoning about HCSP in the duration calculus (2013, submitted)

    Google Scholar 

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

    MATH  Google Scholar 

  38. 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, Berlin (2014). doi:10.1007/978-3-642-54108-7_14

    Chapter  Google Scholar 

Download references

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.

Author information

Authors and Affiliations

  1. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Mingshuai Chen, Shuling Wang & Naijun Zhan

  2. Department of Computer Science, Aalborg University, Aalborg, Denmark

    Anders P. Ravn

  3. Chinese Academy of Space Technology, Beijing, China

    Mengfei Yang

Authors
  1. Mingshuai Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Anders P. Ravn
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Shuling Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mengfei Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. 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. London South Bank University, London, United Kingdom

    Jonathan P. Bowen

  2. East China Normal University, Shanghai, China

    Huibiao Zhu

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Chen, M., Ravn, A.P., Wang, S., Yang, M., Zhan, N. (2017). A Two-Way Path Between Formal and Informal Design of Embedded Systems. In: Bowen, J., Zhu, H. (eds) Unifying Theories of Programming. UTP 2016. Lecture Notes in Computer Science(), vol 10134. Springer, Cham. https://doi.org/10.1007/978-3-319-52228-9_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-52228-9_4

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation