Towards Satisfaction Checking of Power Contracts in Uppaal
Gregor Nitsche and Kim Grüttner and Wolfgang Nebel
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.
12 / 2015
inbook
Springer International Publishing
Lecture Notes in Electrical Engineering
9
157-179
ANCONA
Analog-Coverage in der Nanoelektronik (sorry - only available in german)
Analog-Coverage in der Nanoelektronik (sorry - only available in german)
Frank Oppenheimer and Julio Luis Medina Pasaje
361
OFFIS Autoren
