HaiQ: Synthesis of Software Design Spaces with Structural and Probabilistic Guarantees

Formal methods used to validate software designs, like Alloy, OCL, and B, are powerful tools to analyze complex structures (e.g., architectures, object-relational mappings) captured as sets of relational constraints. However, their applicability is limited when software is subject to uncertainty (derived, e.g., from lack of control over third-party components, interaction with physical elements). In contrast, quantitative verification has emerged as a powerful way of providing quantitative guarantees about the performance, cost, and reliability of systems operating under uncertainty. However, quantitative verification methods do not retain the flexibility of relational modeling in describing structures, forcing engineers to trade structural exploration for analytic capabilities that concern probabilistic and other quantitative guarantees. This paper contributes a method (HaiQ) that enhances structural modeling/synthesis with quantitative guarantees in the style provided by quantitative verification. It includes a language for describing structure and (stochastic) behavior of systems, and a temporal logic that allows checking probability and reward-based properties over sets of feasible design alternatives implicitly described by the relational constraints in a HaiQ model. We report the results of applying a prototype tool in two domains, on which we show the feasibility of synthesizing structural designs that optimize probabilistic and other quantitative guarantees.