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. Winner of the ECSA Best Paper Award.
Online links:   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.
|
|
