Skip to main content

2017 | OriginalPaper | Buchkapitel

Synthesizing SystemC Code from Delay Hybrid CSP

verfasst von : Gaogao Yan, Li Jiao, Shuling Wang, Naijun Zhan

Erschienen in: Programming Languages and Systems

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
The tool and all examples for HCSP and dHCSP can be found at https://​github.​com/​HCSP-CodeGeneration/​HCSP2SystemC.
 
Literatur
6.
Zurück zum Zitat Alur, R., Ivancic, F., Kim, J., Lee, I., Sokolsky, O.: Generating embedded software from hierarchical hybrid models. In: LCTES 2003, pp. 171–182 (2003) Alur, R., Ivancic, F., Kim, J., Lee, I., Sokolsky, O.: Generating embedded software from hierarchical hybrid models. In: LCTES 2003, pp. 171–182 (2003)
7.
Zurück zum Zitat 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)MathSciNetCrossRefMATH 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)MathSciNetCrossRefMATH
8.
Zurück zum Zitat Angeli, D., et al.: A Lyapunov approach to incremental stability properties. IEEE Trans. Autom. Control 47(3), 410–421 (2002)MathSciNetCrossRefMATH Angeli, D., et al.: A Lyapunov approach to incremental stability properties. IEEE Trans. Autom. Control 47(3), 410–421 (2002)MathSciNetCrossRefMATH
9.
Zurück zum Zitat Bellen, A., Zennaro, M.: Numerical Methods for Delay Differential Equations. Oxford University Press, Oxford (2013)MATH Bellen, A., Zennaro, M.: Numerical Methods for Delay Differential Equations. Oxford University Press, Oxford (2013)MATH
10.
Zurück zum Zitat Berry, G.: The foundations of esterel. In: Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 425–454 (2000) Berry, G.: The foundations of esterel. In: Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 425–454 (2000)
12.
Zurück zum Zitat 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 CrossRef 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 CrossRef
13.
Zurück zum Zitat 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 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
14.
Zurück zum Zitat Girard, A., Pappas, G.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782–798 (2007)MathSciNetCrossRefMATH Girard, A., Pappas, G.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782–798 (2007)MathSciNetCrossRefMATH
15.
Zurück zum Zitat Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language lustre. In: Proceedings of the IEEE, pp. 1305–1320 (1991) Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language lustre. In: Proceedings of the IEEE, pp. 1305–1320 (1991)
18.
Zurück zum Zitat Huang, Z., Fan, C., Mitra, S.: Bounded invariant verification for time-delayed nonlinear networked dynamical systems. Nonlinear Anal. Hybrid Syst. 23, 211–229 (2017)MathSciNetCrossRefMATH Huang, Z., Fan, C., Mitra, S.: Bounded invariant verification for time-delayed nonlinear networked dynamical systems. Nonlinear Anal. Hybrid Syst. 23, 211–229 (2017)MathSciNetCrossRefMATH
20.
Zurück zum Zitat Lee, E.: What’s ahead for embedded software? Computer 33(9), 18–26 (2000)CrossRef Lee, E.: What’s ahead for embedded software? Computer 33(9), 18–26 (2000)CrossRef
21.
Zurück zum Zitat 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)CrossRefMATH 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)CrossRefMATH
22.
Zurück zum Zitat 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)MathSciNetCrossRefMATH 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)MathSciNetCrossRefMATH
23.
Zurück zum Zitat Prajna, S., Jadbabaie, A.: Methods for safety verification of time-delay systems. In: CDC 2005, pp. 4348–4353 (2005) Prajna, S., Jadbabaie, A.: Methods for safety verification of time-delay systems. In: CDC 2005, pp. 4348–4353 (2005)
26.
Zurück zum Zitat Yan, G., Jiao, L., Wang, L., Wang, S., Zhan, N.: Automatically generating SystemC code from HCSP formal models (Submitted) Yan, G., Jiao, L., Wang, L., Wang, S., Zhan, N.: Automatically generating SystemC code from HCSP formal models (Submitted)
27.
Zurück zum Zitat Zhan, N., Wang, S., Zhao, H.: Formal Verification of Simulink/Stateflow Diagrams: A Deductive Way. Springer, New York (2016) Zhan, N., Wang, S., Zhao, H.: Formal Verification of Simulink/Stateflow Diagrams: A Deductive Way. Springer, New York (2016)
Metadaten
Titel
Synthesizing SystemC Code from Delay Hybrid CSP
verfasst von
Gaogao Yan
Li Jiao
Shuling Wang
Naijun Zhan
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-71237-6_2

Premium Partner