Automated Reliability Prediction from Formal Architectural Descriptions

Quantitative assessment of quality attributes (i.e., non-functional requirements, such as performance, safety or reliability) of software architectures during design supports important early decisions and validates the quality requirements established by the stakeholder. In current practice, these quality requirements are most often manually checked, which is time-consuming and error-prone due to the overwhelmingly complex designs. We propose an automated approach to assess the reliability of software architectures. It consists in extracting a Markov model from the system specification written in an Architecture Description Language (ADL). Our approach translates the specified architecture to a high-level probabilistic model-checking language, supporting system validation and quantitative reliability prediction against usage profile, component arrangement and architectural styles. We validate our approach by applying it to different architectural styles and comparing those with two different quantitative reliability assessment methods presented in the literature: the composite and the hierarchical methods.