Top

Published in:

2016 | OriginalPaper | Chapter

9. Towards Satisfaction Checking of Power Contracts in Uppaal

Authors : Gregor Nitsche, Kim Grüttner, Wolfgang Nebel

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

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

previous chapter A Framework for Distributed, Loosely-Synchronized Simulation of Complex SystemC/TLM Models

next chapter SystemC AMS Power Electronic Modelling with Ideal Instantaneous Switches

Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2) (1994). doi:10.1016/0304-3975(94)90010-8

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

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

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)

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)

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)

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)

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

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 Specification^TM, version 2.0 edn. Silicon Integration Initiative, Inc. (Si2^TM) (2011)

24.

UPPAAL: http://www.uppaal.org/

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

Title: Towards Satisfaction Checking of Power Contracts in Uppaal
Authors: Gregor Nitsche
Kim Grüttner
Wolfgang Nebel
Publisher: Springer International Publishing
Book: Languages, Design Methods, and Tools for Electronic System Design
Print ISBN: 978-3-319-24455-6

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

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