Availability Evaluation of Software Architectures through Formal Methods

The quantitative assessment of quality attributes on software architectures allow to support early decisions in the design phase, certify quality requirements established by stakeholders and improve software quality in future architectural changes. In literature, only few of these quality requirements are verified and most often they are manually checked, which is time-consuming and error-prone due to the overwhelmingly complex designs. The goal of this thesis is to provide means for architects predict and analyze availability constraints on software architectures. We plan to generate a stochastic model from an architectural description specified by an Architecture Description Language (ADL) properly annotated to be solved by a probabilistic model-checking tool. This model will allow to quantitatively predict availability and identify bottlenecks that are negatively influencing the overall system availability. Hence, our approach will help architects to avoid undesired or infeasible architectural designs and prevent extra costs in fixing late life-cycle detected problems.