Artifacts for "System Architecture Synthesis for Performability by Logic Solvers"

Our paper proposes two logic solver-based approaches to evaluate complex design spaces by using partial models in order to find an optimal solution with respect to performability objectives. One approach uses performability analysis as a post-filtering of valid system architecture candidates, while the other approach uses performability analysis for guiding the actual search over partial models. Our approaches are implemented in a prototype tool based on the VIATRA-Solver framework and using the PRISM Stochastic Model Checker for performability analysis. We evaluate both approaches on an interferometry mission architecture case study using view transformations for performability analysis and compare our approach with the well-known MOMoT framework based on meta-heuristic search. The artifact contains source code, a Docker image for running the experiments, and a virtual machine for data analysis.