Project B03: Formal Methods for Quantitative Analysis and Optimization of Energy Models
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
- 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
Postdoc
PhD Students
former staff