@inbookGre2015, Author = {Gregor Nitsche and Kim Grüttner and Wolfgang Nebel }, Title = {Towards Satisfaction Checking of Power Contracts in Uppaal}, Year = {2015}, Pages = {157-179}, Month = {12}, Editor = {Frank Oppenheimer and Julio Luis Medina Pasaje}, Publisher = {Springer International Publishing}, Series = {Lecture Notes in Electrical Engineering}, Edition = {361}, chapter = {9}, Doi = {10.1007/978-3-319-24457-0_9}, Url = {http://dx.doi.org/10.1007/978-3-319-24457-0_9}, type = {inbook}, note = {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 desi}, 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.} @COMMENTBibtex file generated on