@inproceedings{Gre2014,
Author = {Gregor Nitsche and Kim Grüttner and Wolfgang Nebel},
Title = {Towards Satisfaction Checking of Power Contracts in Uppaal},

Year = {2014},
Month = {10},
Booktitle = {Forum on specification \& Design Languages (FDL 2014)},
type = {inproceedings},
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 Contract, 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 leafcomponents 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.}
}
@COMMENT{Bibtex file generated on }