Combining Stochastic Process Algebras and Queueing Networks for Software Architecture Analysis

We propose an integrated approach to the functional and performance analysis of Software Architectures (SAs) based on Stochastic Process Algebras (SPAs) and Queueing Networks (QNs), in order to combine their main advantages: formal techniques for the verification of functional properties of systems for SPAs, and efficient performance analysis for QNs. We first introduce Æmilia, a SPA based architectural description language for the compositional, graphical and hierarchical modeling of SAs, which is equipped with suitable checks for the detection of architectural mismatches. Then we present a systematic approach to derive QN models from Æmilia specifications. This is based on the identification of three different classes of QN basic elements --- arrival processes, buffers, and service processes --- and on syntactic restrictions to be imposed to Æmilia specifications, so that each architectural component directly falls into one of the three classes. Although performance analysis could be carried out directly on the Markov chain (MC) underlying an Æmilia specification, having a QN model allows performance indices to be evaluated possibly by exact product form solutions or by well known approximate methods. Furthermore, unlike the underlying MC, the high level of abstraction of the QN model should ease the interpretation of the performance results at the architectural description level.