The goal of this project is to develop the foundations for using probabilistic model checking (PMC) for the analysis of layer-wise and cross-layer energy-management strategies. We will develop new theory, algorithms and implementations for PMC-based multi-objective analysis and novel modeling concepts for compositional reasoning about energy-utility trade-offs. We will explore integrating PMC results into the energy-control loop to support decision making at runtime, carry out case studies with the project partners and investigate combining PMC and description-logic reasoning.

Role within the CRC 912

© CRC 912

• A04: With A04 we collaborated on an operational semantics of MPI (message passing interface) specifications.
• B01: In collaboration with B01, we will refine our initial work on a model of aspects of SLAM, with an eye on the energy-utility characteristics.
• B02: There is also collaboration with B02 addressing the combination of model-checking techniques and description logic reasoners.
• B04: We analysed the energy, performance and correctness of several locking protocols and an energy-aware bonding network device together with B04. Furthermore, we laid the foundations for the formalisation of layered performance/demand models.
• HAEC-Software-Group: Together with all B-partners we worked on the HAECubie joint demonstrator with video downloading and transcoding as an application. This serves as a showpiece for illustrating the interplay of the different projects within the HAEC-Software group to achieve our global goal of energy-efficiency and energy-proportionality at runtime.

Staff

Principal Investigator

• Prof. Dr. Christel Baier

Postdoc

• Dr.-Ing. Sascha Klüppelholz
• Dr. rer. nat. Joachim Klein

PhD Students

• M. Sc. Philipp Chrszon

former staff

• Dipl.-Inf. Marcus Daum