Skip to main content
SpringerLink
Log in

Synthesizing SystemC Code from Delay Hybrid CSP

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2017)

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

Included in the following conference series:

  • 876 Accesses

Abstract

Delay is omnipresent in modern control systems, which can prompt oscillations and may cause deterioration of control performance, invalidate both stability and safety properties. This implies that safety or stability certificates obtained on idealized, delay-free models of systems prone to delayed coupling may be erratic, and further the incorrectness of the executable code generated from these models. However, automated methods for system verification and code generation that ought to address models of system dynamics reflecting delays have not been paid enough attention yet in the computer science community. In our previous work, on one hand, we investigated the verification of delay dynamical and hybrid systems; on the other hand, we also addressed how to synthesize SystemC code from a verified hybrid system modelled by Hybrid CSP (HCSP) without delay. In this paper, we give a first attempt to synthesize SystemC code from a verified delay hybrid system modelled by Delay HCSP (dHCSP), which is an extension of HCSP by replacing ordinary differential equations (ODEs) with delay differential equations (DDEs). We implement a tool to support the automatic translation from dHCSP to SystemC.

This work is partially supported by “973 Program” under grant No. 2014CB340701, by NSFC under grants 61625206, 61732001 and 91418204, by CDZ project CAP (GZ 1023), 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.

    The tool and all examples for HCSP and dHCSP can be found at https://github.com/HCSP-CodeGeneration/HCSP2SystemC.

References

  1. Rational Rose. http://www-03.ibm.com/software/products/en/rosemod

  2. Simulink. https://cn.mathworks.com/products/simulink.html

  3. TargetLink. https://www.dspace.com/en/inc/home/products/sw/pcgs/targetli.cfm

  4. Ahmad, E., Dong, Y., Wang, S., Zhan, N., Zou, L.: Adding formal meanings to AADL with hybrid annex. In: Lanese, I., Madelaine, E. (eds.) FACS 2014. LNCS, vol. 8997, pp. 228–247. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15317-9_15

    Google Scholar 

  5. Alur, R., Grosu, R., Hur, Y., Kumar, V., Lee, I.: Modular specification of hybrid systems in charon. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 6–19. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46430-1_5

    Chapter  Google Scholar 

  6. Alur, R., Ivancic, F., Kim, J., Lee, I., Sokolsky, O.: Generating embedded software from hierarchical hybrid models. In: LCTES 2003, pp. 171–182 (2003)

    Google Scholar 

  7. Anand, M., Fischmeister, S., Hur, Y., Kim, J., Lee, I.: Generating reliable code from hybrid-systems models. IEEE Trans. Comput. 59(9), 1281–1294 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  8. Angeli, D., et al.: A Lyapunov approach to incremental stability properties. IEEE Trans. Autom. Control 47(3), 410–421 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  9. Bellen, A., Zennaro, M.: Numerical Methods for Delay Differential Equations. Oxford University Press, Oxford (2013)

    MATH  Google Scholar 

  10. Berry, G.: The foundations of esterel. In: Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 425–454 (2000)

    Google Scholar 

  11. Chen, M., Fränzle, M., Li, Y., Mosaad, P.N., Zhan, N.: Validated simulation-based verification of delayed differential dynamics. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 137–154. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_9

    Chapter  Google Scholar 

  12. Deshpande, A., Göllü, A., Varaiya, P.: SHIFT: a formalism and a programming language for dynamic networks of hybrid automata. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1996. LNCS, vol. 1273, pp. 113–133. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0031558

    Chapter  Google Scholar 

  13. Fränzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J. Satisf. Boolean Model. Comput. 1, 209–236 (2007)

    MATH  Google Scholar 

  14. Girard, A., Pappas, G.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782–798 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  15. Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language lustre. In: Proceedings of the IEEE, pp. 1305–1320 (1991)

    Google Scholar 

  16. Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  17. Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 1–15. Springer, Heidelberg (2006). https://doi.org/10.1007/11813040_1

    Chapter  Google Scholar 

  18. Huang, Z., Fan, C., Mitra, S.: Bounded invariant verification for time-delayed nonlinear networked dynamical systems. Nonlinear Anal. Hybrid Syst. 23, 211–229 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  19. Hur, Y., Kim, J., Lee, I., Choi, J.-Y.: Sound code generation from communicating hybrid models. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 432–447. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24743-2_29

    Chapter  Google Scholar 

  20. Lee, E.: What’s ahead for embedded software? Computer 33(9), 18–26 (2000)

    Article  Google Scholar 

  21. Pola, G., Pepe, P., Di Benedetto, M.: Symbolic models for nonlinear time-varying time-delay systems via alternating approximate bisimulation. Int. J. Robust Nonlinear Control 25(14), 2328–2347 (2015)

    Article  MATH  Google Scholar 

  22. Pola, G., Pepe, P., Di Benedetto, M., Tabuada, P.: Symbolic models for nonlinear time-delay systems using approximate bisimulations. Syst. Control Lett. 59(6), 365–373 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  23. Prajna, S., Jadbabaie, A.: Methods for safety verification of time-delay systems. In: CDC 2005, pp. 4348–4353 (2005)

    Google Scholar 

  24. Yan, G., Jiao, L., Li, Y., Wang, S., Zhan, N.: Approximate bisimulation and discretization of hybrid CSP. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 702–720. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_43

    Chapter  Google Scholar 

  25. Yan, G., Jiao, L., Wang, S., Zhan, N.: Synthesizing SystemC code from delay hybrid CSP (full version). https://www.dropbox.com/s/rxbrib49bx1yv60/APLAS2017-FULL.pdf?dl=0

  26. Yan, G., Jiao, L., Wang, L., Wang, S., Zhan, N.: Automatically generating SystemC code from HCSP formal models (Submitted)

    Google Scholar 

  27. Zhan, N., Wang, S., Zhao, H.: Formal Verification of Simulink/Stateflow Diagrams: A Deductive Way. Springer, New York (2016)

    Google Scholar 

  28. Zou, L., Fränzle, M., Zhan, N., Mosaad, P.N.: Automatic verification of stability and safety for delay differential equations. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 338–355. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3_20

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Gaogao Yan, Li Jiao, Shuling Wang & Naijun Zhan

  2. University of Chinese Academy of Sciences, Beijing, China

    Gaogao Yan & Naijun Zhan

Authors
  1. Gaogao Yan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Li Jiao
    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. Naijun Zhan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Shuling Wang or Naijun Zhan .

Editor information

Editors and Affiliations

  1. University of Colorado, Boulder, Colorado, USA

    Bor-Yuh Evan Chang

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Yan, G., Jiao, L., Wang, S., Zhan, N. (2017). Synthesizing SystemC Code from Delay Hybrid CSP. In: Chang, BY. (eds) Programming Languages and Systems. APLAS 2017. Lecture Notes in Computer Science(), vol 10695. Springer, Cham. https://doi.org/10.1007/978-3-319-71237-6_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-71237-6_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-71236-9

  • Online ISBN: 978-3-319-71237-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation