Greener Bits: Formal Analysis of Demand Response

• Christel Baier, Sascha Klüppelholz, Hermann de Meer, Florian Niedermeier and Sascha Wunderlich:
  Greener Bits: Formal Analysis of Demand Response (ATVA'16, Springer)
• Christel Baier, Sascha Klüppelholz, Hermann de Meer, Florian Niedermeier and Sascha Wunderlich:
  Greener Bits: Formal Analysis of Demand Response (extended version)

Sources of PRISM and ProFeat

To replicate the experimental results, PRISM version 4.3 with additional unpublished patches is needed. Additionally, ProFeat version 0.100.0 or higher is necessary to generate the model. Pre-generated versions of the model can be found below.

Feel free to contact us for a copy of the tools.

Experiments

Logs, the used models and properties and the tooling to generate them (except PRISM and ProFeat binaries).
To use them, do the following:

• extract the tooling
• extract the models and properties into a subdirectory "static" (or create your own)
• put the binaries mentioned in the makefile into a subdirectory "bin"