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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Automatic Refinement Checking for Formal System Models Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

9. Towards Satisfaction Checking of Power Contracts in Uppaal

verfasst von : Gregor Nitsche, Kim Grüttner, Wolfgang Nebel

Erschienen in: Languages, Design Methods, and Tools for Electronic System Design

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Since energy consumption is one of the most limiting factors for embedded and integrated systems, today’s microelectronic design demands urgently for power-aware methodologies for early specification, design-space exploration, and verification of the designs’ power properties. To this end, we currently develop a contract- and component-based design concept for power properties, called power contractss, to provide a formal link between the bottom-up power characterization of low-level system components and the top-down specification of the systems’ high-level power intent. In this paper, we present a first proof of concept for the verification of the leaf-component power contracts of a hierarchical system design w.r.t. their implementation in UPPAAL. Building on these, we can provide assured power contracts for the hierarchical virtual integration (VI) of the leaf-components to a compound power contract of the integrated final system and thus allow for a sound and traceable bottom-up integration and verification methodology for power properties.

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
Vorheriges Kapitel A Framework for Distributed, Loosely-Synchronized Simulation of Complex SystemC/TLM Models
Nächstes Kapitel SystemC AMS Power Electronic Modelling with Ideal Instantaneous Switches
Literatur
1.
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2) (1994). doi:10.1016/0304-3975(94)90010-8
2.
Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Formal Methods for the Design of Real-Time Systems. Springer, Berlin (2004)CrossRefMATH
3.
Ben Abdallah, F., Apvrille, L.: Fast evaluation of power consumption of embedded systems using DIPLODOCUS. In: 39th EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA’13) (2013). doi:10.1109/SEAA.2013.8
4.
Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets, Lecture Notes in Computer Science, vol. 3098. Springer, Berlin/Heidelberg (2004)
5.
Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T., Larsen, K.: Contracts for systems design. Technical Report RR-8147, Research Centre Rennes—Bretagne Atlantique, Rennes Cedex (2012)
6.
Boudjadar, J., David, A., Kim, J.H., Larsen, K.G., Mikucionis, M., Nyman, U., Skou, A.: Schedulability and energy efficiency for multi-core hierarchical scheduling systems. In: Proceedings of the Conference on Embedded Real Time Systems and Software (ERTSS’14). Toulouse (2014)
7.
Damm, W., Dierks, H., Oehlerking, J., Pnueli, A.: Towards component based design of hybrid systems: Safety and stability. In: Manna, Z., Peled, D.A. (eds.) Time for Verification Essays in Memory of Amir Pnueli. Lecture Notes in Computer Science, vol. 6200. Springer, Berlin/Heidelberg (2010)
8.
Damm, W., Hungar, H., Josko, B., Peikenkamp, T., Stierand, I.: Using contract–based component specifications for virtual integration testing and architecture design. In: Lukasiewycz, M., Chakraborty, S., Milbredt, P. (eds.) Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE), 2011. Grenoble, France (2011). doi:10.1109/DATE.2011.5763167
9.
David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: Proceedings of the 13th ACM international conference on Hybrid systems: computation and control, HSCC ’10. New York (2010). doi:10. 1145/1755952.1755967
10.
Gomez, C., DeAntoni, J., Mallet, F.: Power consumption analysis using multi-view modeling. In: Proceedings of the 23rd International Workshop on Power and Timing Modeling, Optimization and Simulation (PATMOS). IEEE, Karlsruhe (2013)
11.
Holzmann, G.J.: Design And Validation Of Computer Protocols. Prentice Hall, New Jersey (2007)
12.
Hungar, H.: Components and contracts: a semantical foundation for compositional refinement. In: Tagungsband MBEES: Modellbasierte Entwicklung eingebetteter Systeme 2012 (2012)
13.
IEEE Computer Society, Design Automation Committee, IEEE Standards Association, Corporate Advisory Group, Institute of Electrical and Electronics Engineers, IEEE-SA Standards Board: IEEE Standard for Design and Verification of Low-Power Integrated Circuits. IEEE Standards Association, New Jersey (2013)
14.
Josko, B., Ma, Q., Metzner, A.: Designing embedded systems using heterogeneous rich components. In: Proceedings of the INCOSE International Symposium (2008)
15.
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. In: Proceedings of the 2nd Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 1055. Springer, Berlin (1995)
16.
Lee, E.A., Sangiovanni-vincentelli, A.: The tagged signal model - a preliminary version of a denotational framework for comparing models of computation. Technical Report UCB/ERL M96/33, University of California, Berkeley, CA (1996)
17.
Lee, E., Sangiovanni-Vincentelli, A.: A framework for comparing models of computation. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. 17(12) (1998). doi:10.1109/43.736561
18.
Liu, X.: Semantic foundation of the tagged signal model. Ph.D. thesis, EECS Department, University of California, Berkeley, (2005)
19.
Lorenz, D., Grüttner, K., Bombieri, N., Guarnieri, V., Bocchio, S.: From RTL IP to functional system-level models with extra-functional properties. In: Jerraya, A., Carloni, L.P., Chang, N., Fummi, F. (eds.) Proceedings of the Eighth IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS ’12. ACM, New York, NY (2012). doi:10.1145/2380445.2380529
20.
Lorenz, D., Hartmann, P.A., Grüttner, K., Nebel, W.: Non-invasive power simulation at system-level with SystemC. In: Ayala, J.L., Shang, D., Yakovlev, A. (eds.) Proceedings of the International Workshop on Power and Timing Modeling, Optimization and Simulation (PATMOS) 2012. Lecture Notes in Computer Science, vol. 7606. Springer, Newcastle upon Tyne (2012)
21.
Nitsche, G., Grüttner, K., Nebel, W.: Power contracts: a formal way towards power–closure?! In: Proceedings of the 23rd International Workshop on Power and Timing Modeling, Optimization and Simulation (PATMOS’13). IEEE, Karlsruhe (2013)
22.
Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: contract-based design for cyber-physical systems. Eur. J. Control 18(3) (2012). doi:10.3166/ejc.18.217-238
23.
Silicon Integration Initiative, I.S.: Si2 Common Power Format SpecificationTM, version 2.0 edn. Silicon Integration Initiative, Inc. (Si2TM) (2011)
24.
25.
Urdahl, J., Stoffel, D., Kunz, W.: Path predicate abstraction for sound system-level models of RT-level circuit designs. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. 33(2) (2014). doi:10.1109/ TCAD.2013.2285276
Metadaten
Titel
Towards Satisfaction Checking of Power Contracts in Uppaal
verfasst von
Gregor Nitsche
Kim Grüttner
Wolfgang Nebel
Copyright-Jahr
2016
Buch
Languages, Design Methods, and Tools for Electronic System Design

Print ISBN: 978-3-319-24455-6

Electronic ISBN: 978-3-319-24457-0

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-24457-0_9

Neuer Inhalt

    Bildnachweise