Skip to main content

2018 | OriginalPaper | Buchkapitel

Integrating Simulink Models into the Model Checker Cosmos

verfasst von : Benoît Barbot, Béatrice Bérard, Yann Duplouy, Serge Haddad

Erschienen in: Application and Theory of Petri Nets and Concurrency

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

We present an implementation for Simulink model executions in the statistical model-checker Cosmos. We take profit of this implementation for hybrid modeling and simulations combining Petri nets and Simulink models.

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!

Literatur
1.
Zurück zum Zitat Agrawal, A., Simon, G., Karsai, G.: Semantic translation of simulink/stateflow models to hybrid automata using graph transformations. Electr. Notes Theor. Comput. Sci. 109, 43–56 (2004)CrossRef Agrawal, A., Simon, G., Karsai, G.: Semantic translation of simulink/stateflow models to hybrid automata using graph transformations. Electr. Notes Theor. Comput. Sci. 109, 43–56 (2004)CrossRef
2.
Zurück zum Zitat Ballarini, P., Barbot, B., Duflot, M., Haddad, S., Pekergin, N.: HASL: a new approach for performance evaluation and model checking from concepts to experimentation. Perform. Eval. 90, 53–77 (2015)CrossRef Ballarini, P., Barbot, B., Duflot, M., Haddad, S., Pekergin, N.: HASL: a new approach for performance evaluation and model checking from concepts to experimentation. Perform. Eval. 90, 53–77 (2015)CrossRef
3.
Zurück zum Zitat Ballarini, P., Duflot, M.: Applications of an expressive statistical model checking approach to the analysis of genetic circuits. Theor. Comput. Sci. 599, 4–33 (2015)MathSciNetCrossRef Ballarini, P., Duflot, M.: Applications of an expressive statistical model checking approach to the analysis of genetic circuits. Theor. Comput. Sci. 599, 4–33 (2015)MathSciNetCrossRef
7.
Zurück zum Zitat Barbot, B., Haddad, S., Heiner, M., Picaronny, C.: Rare event handling in signalling cascades. Int. J. Adv. Syst. Meas. 8(1–2), 69–79 (2015) Barbot, B., Haddad, S., Heiner, M., Picaronny, C.: Rare event handling in signalling cascades. Int. J. Adv. Syst. Meas. 8(1–2), 69–79 (2015)
9.
Zurück zum Zitat Barbot, B., Kwiatkowska, M., Mereacre, A., Paoletti, N.: Building power consumption models from executable timed I/O automata specifications. In: Proceedings of HSCC 2016, pp. 195–204. ACM (2016) Barbot, B., Kwiatkowska, M., Mereacre, A., Paoletti, N.: Building power consumption models from executable timed I/O automata specifications. In: Proceedings of HSCC 2016, pp. 195–204. ACM (2016)
10.
Zurück zum Zitat Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: Non-standard semantics of hybrid systems modelers. J. Comput. Syst. Sci. 78(3), 877–910 (2012)MathSciNetCrossRef Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: Non-standard semantics of hybrid systems modelers. J. Comput. Syst. Sci. 78(3), 877–910 (2012)MathSciNetCrossRef
11.
Zurück zum Zitat Bouissou, O., Chapoutot, A.: An operational semantics for simulink’s simulation engine. In: Proceedings of the 13th ACM SIGPLAN/SIGBED, LCTES 2012, pp. 129–138. ACM, New York (2012) Bouissou, O., Chapoutot, A.: An operational semantics for simulink’s simulation engine. In: Proceedings of the 13th ACM SIGPLAN/SIGBED, LCTES 2012, pp. 129–138. ACM, New York (2012)
12.
Zurück zum Zitat Chow, Y.S., Robbins, H.: On the asymptotic theory of fixed-width sequential confidence intervals for the mean. Ann. Math. Stat. 36, 457–462 (1965)MathSciNetCrossRef Chow, Y.S., Robbins, H.: On the asymptotic theory of fixed-width sequential confidence intervals for the mean. Ann. Math. Stat. 36, 457–462 (1965)MathSciNetCrossRef
13.
Zurück zum Zitat Clopper, C., Pearson, E.S.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26, 404–413 (1934)CrossRef Clopper, C., Pearson, E.S.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26, 404–413 (1934)CrossRef
14.
Zurück zum Zitat Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13–30 (1963)MathSciNetCrossRef Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13–30 (1963)MathSciNetCrossRef
15.
Zurück zum Zitat Tiwari, A.: Formal semantics and analysis methods for simulink stateflow models. Technical report, SRI (2002) Tiwari, A.: Formal semantics and analysis methods for simulink stateflow models. Technical report, SRI (2002)
16.
Zurück zum Zitat Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Embed. Comput. Syst. 4(4), 779–818 (2005)CrossRef Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Embed. Comput. Syst. 4(4), 779–818 (2005)CrossRef
Metadaten
Titel
Integrating Simulink Models into the Model Checker Cosmos
verfasst von
Benoît Barbot
Béatrice Bérard
Yann Duplouy
Serge Haddad
Copyright-Jahr
2018
DOI
https://doi.org/10.1007/978-3-319-91268-4_19