SHOW publication #578 - ABLE Publications

Designing software in a way that guarantees run-time behavior while achieving an acceptable balance among multiple quality attributes is an open problem. Providing guarantees about the satisfaction of the same requirements under uncertain environments is even more challenging. Tools and techniques to inform engineers about poorly-understood design spaces in the presence of uncertainty are needed, so that engineers can explore the design space, especially when tradeoffs are crucial. To tackle this problem, we describe an approach that combines synthesis of spaces of system design alternatives from formal specifications of architectural styles with probabilistic formal verification. 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) subject to uncertainty, which is treated as a first-class entity. We illustrate our approach in two case studies: a service-based adaptive system and a mobile robotics architecture. Our results show how the framework can provide useful insights into how average case probabilistic guarantees can differ from worst case guarantees, emphasizing the relevance of combining quantitative formal verification methods with structural synthesis, in contrast with techniques based on simulation and dynamic analysis that can only provide estimates about average case probabilistic properties.