SAFARE is a tool for systematic design of Data Aggregation Processes (DAP). It provides interface to design DAP based on DAGGTAX (Data AGGregation TAXonomy) , and integrates the Microsoft Z3 Theorem Prover  to check the consistency of the design solution.
The source code and documentation of SAFARE can be downlowded here .
1. Cai, S., Gallina, B., Nyström, D., Seceleanu, C., Larsson, A.: Tool-supported design of data aggregation processes in cloud monitoring systems. Journal of Ambient Intelligence and Humanized Computing pp. 1–17 (2018)
2. De Moura, L., Bjørner, N.: Z3: An efficient smt solver. Tools and Algorithms for the Construction and Analysis of Systems pp. 337–340 (2008)