Specification driven tradespace analysis

This paper contributes experimental results suggesting that formal synthesis of large spaces of software designs from relational logic specifications, combined with large-scale dynamic analysis of the synthesized designs, tends to reveal significantly better designs than those produced by widely used methods. The results in this paper are from the particular domain of object-relation mapping (ORM). Our experiments were enabled by a novel, general, and formal framework for automated design synthesis and dynamic trade-space analysis. We instantiated it to create an ORM-specific apparatus for our experiments. We present the design and evaluation of this framework as a second contribution of this work.