Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Automated Analysis of Asynchronously Communicating Systems Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Compositional Semantics and Analysis of Hierarchical Block Diagrams

verfasst von : Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis

Erschienen in: Model Checking Software

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We present a compositional semantics and analysis framework for hierarchical block diagrams (HBDs) in terms of atomic and composite predicate transformers. Our framework consists of two components: (1) a compiler that translates Simulink HBDs into an algebra of transformers composed in series, in parallel, and in feedback; (2) an implementation of the theory of transformers and static analysis techniques for them in Isabelle. We evaluate our framework on several case studies including a benchmark Simulink model by Toyota.

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Symbolic Game Semantics for Model Checking Program Families
Nächstes Kapitel Using SPIN for the Optimized Scheduling of Discrete Event Systems in Manufacturing
Fußnoten
3
Our exposition focuses on HBDs as implemented in Simulink, but our method and tool can also be applied to other block-diagram based languages with minor changes.
 
6
\(\mathcal {T}_{\text{ trans }}\) for NFBT is almost twice larger than for FPT, IT and IT-IO. The reason is that NFBT executes extra steps, such as splitting blocks with multiple outputs and removing CPTs that are not used in calculating the system’s output.
 
Literatur
1.
Agrawal, A., Simon, G., Karsai, G.: Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations. Electron. Notes Theor. Comput. Sci. 109, 43–56 (2004)CrossRefMATH
2.
Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998)CrossRefMATH
3.
Boström, P.: Contract-based verification of Simulink models. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 291–306. Springer, Heidelberg (2011)CrossRef
4.
Chen, C., Dong, J.S., Sun, J.: A formal framework for modeling and validating Simulink diagrams. Formal Aspects Comput. 21(5), 451–483 (2009)CrossRefMATH
5.
Cook, J.A., Sun, J., Buckland, J.H., Kolmanovsky, I.V., Peng, H., Grizzle, J.W.: Automotive powertrain control - A survey. Asian J. Control 8(3), 237–260 (2006)MathSciNetCrossRef
6.
7.
Dragomir, I., Preoteasa, V., Tripakis, S.: Translating hierarchical block diagrams into composite predicate transformers. CoRR, abs/1510.04873 (2015)
8.
Frehse, G., Han, Z., Krogh, B.: Assume-guarantee reasoning for hybrid I/O-automata by over-approximation of continuous interaction. In: CDC, pp. 479–484 (2004)
9.
Garavel, H., Sighireanu, M.: A graphical parallel composition operator for process algebras. In: FORTE XII. IFIP Conference Proceedings, vol. 156, pp. 185–202. Kluwer (1999)
10.
Jin, X., Deshmukh, J., Kapinski, J., Ueda, K., Butts, K.: Benchmarks for model transformations and conformance checking. In: ARCH (2014)
11.
Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain control verification benchmark. In: HSCC, pp. 253–262. ACM (2014)
12.
Lee, E., Messerschmitt, D.: Synchronous data flow. Proc. IEEE 75(9), 1235–1245 (1987)CrossRef
13.
Lublinerman, R., Szegedy, C., Tripakis, S.: Modular code generation from synchronous block diagrams - modularity vs. code size. In: POPL, pp. 78–89. ACM, January 2009
14.
Lublinerman, R., Tripakis, S.: Modularity vs. reusability: code generation from synchronous block diagrams. In: DATE, pp. 1504–1509. ACM, March 2008
15.
16.
Manamcheri, K., Mitra, S., Bak, S., Caccamo, M.: A step towards verification and synthesis from Simulink/Stateflow models. In: HSCC, pp. 317–318. ACM (2011)
17.
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)CrossRef
18.
Minopoli, S., Frehse, G.: SL2SX Translator: from Simulink to SpaceEx verification tool. In: HSCC (2016)
19.
Preoteasa, V., Tripakis, S.: Refinement calculus of reactive systems. In: EMSOFT, pp. 1–10, October 2014
20.
Preoteasa, V., Tripakis, S.: Towards compositional feedback in non-deterministic and non-input-receptive systems. CoRR, abs/1510.06379 (2015)
21.
Roy, P., Shankar, N.: SimCheck: a contract type system for Simulink. Innovations Syst. Softw. Eng. 7(2), 73–83 (2011)CrossRef
22.
Sfyrla, V., Tsiligiannis, G., Safaka, I., Bozga, M., Sifakis, J.: Compositional translation of Simulink models into synchronous BIP. In: SIES, pp. 217–220, July 2010
23.
Tripakis, S., Lickly, B., Henzinger, T.A., Lee, E.A.: A theory of synchronous relational interfaces. ACM Trans. Program. Lang. Syst. 33(4), 14:1–14:41 (2011)CrossRef
24.
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
25.
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)CrossRef
26.
Zhou, C., Kumar, R.: Semantic translation of Simulink diagrams to input/output extended finite automata. Discrete Event Dyn. Syst. 22(2), 223–247 (2012)MathSciNetCrossRefMATH
27.
Zou, L., Zhany, N., Wang, S., Franzle, M., Qin, S.: Verifying Simulink diagrams via a hybrid Hoare logic prover. In: EMSOFT, pp. 9:1–9:10, September 2013
Metadaten
Titel
Compositional Semantics and Analysis of Hierarchical Block Diagrams
verfasst von
Iulia Dragomir
Viorel Preoteasa
Stavros Tripakis
Copyright-Jahr
2016
Buch
Model Checking Software

Print ISBN: 978-3-319-32581-1

Electronic ISBN: 978-3-319-32582-8

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-32582-8_3