A General Algebraic Theory and Derived Software Framework for Automated Tradeoff Analysis Tools

This paper presents a formal, general algebraic theory of design space tradeoff analysis tools, and a map-reduce-based framework, derived mechanically from the theory, for implementing such tools. The theory is organized as a hierarchy of Coq typeclasses in a style similar to that being used elsewhere to formalize abstract mathematics. From this theory, using Coq's extraction function, we produce a polymorphic framework (in Scala) that developers specialize and extend to produce domain-specific trade-off analysis tools. As a test and demonstration, we instantiated this framework using code re-engineered from an earlier, ad hoc, only partially automated system for tradeoff analysis of object-relation mappings. Our new tool reduced the time taken by one analysis from weeks to hours.

Tang, Chong, Kevin Sullivan, Hamid Bagheri, and Ke Dou. "A General Algebraic Theory and Derived Software Framework for Automated Tradeoff Analysis Tools." University of Virginia Dept. of Computer Science Tech Report (2014).