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

Abstract

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.