Home   Research Publications Members Related Software
IndexBrowse   BibliographiesMy selection
 Search: in   (word length ≥ 3)
      Login
Publication no #515   Download bibtex file Type :   Html | Bib | Both
Add to my selection
Synthesis and Quantitative Verification of Tradeoff Spaces for Families of Software Systems

Javier Cámara, David Garlan and Bradley Schmerl.


In Proceedings of the 11th European Conference on Software Architecture, Cantebury, UK, 11-15 September 2017. To appear.

Online links: PDF   Bibtex entry   Plain Text

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.

Keywords: Architectural Style, Formal Methods, Model Checking, Software Architecture.  
    Created: 2017-04-25 17:49:20     Modified: 2017-06-28 17:02:27
Feedback: ABLE Webmaster
Last modified: Tue June 20 2017 16:43:41
        BibAdmin