@InProceedings{2017:Camara:ArchitectureSynthesis,
      AUTHOR = {C\'{a}mara, Javier and Garlan, David and Schmerl, Bradley},
      TITLE = {Synthesis and Quantitative Verification of Tradeoff Spaces for Families of Software Systems},
      YEAR = {2017},
      MONTH = {11-15 September},
      BOOKTITLE = {Proceedings of the 11th European Conference on Software Architecture},
      ADDRESS = {Cantebury, UK},
      PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/cgsecsa17.pdf},
      ABSTRACT = {Designing software in a way that provides guarantees about run-time behavior while achieving an acceptable balance between multiple extra-functional properties is still an open problem. Tools and techniques to inform engineers about poorly-understood design spaces are needed. To tackle this problem, we propose an approach that combines synthesis of spaces of system design alternatives from formal specifications of architectural styles with quantitative verification applied to every point of the generated solution space. The main contribution of this paper is a formal framework for specification-driven synthesis and analysis of design spaces that provides formal guarantees about the correctness of system behaviors and satisfies quantitative properties (e.g., defined over system qualities). We illustrate our proposal by analyzing the configuration space of a Tele Assistance System (TAS) using a prototype implementation of our approach.},
      NOTE = {Winner of the ECSA Best Paper Award},
      KEYWORDS = {Architectural Style, Formal Methods, Model Checking, Software Architecture}
}