Combining Stochastic Process Algebras andQueueing Networks for Software Architecture AnalysisSimonetta BalsamoDipartimento di InformaticaUniv. "Ca’ Foscari" di [email protected] BernardoCentro per l’Appl. delle S.T.I.Univ. di [email protected] SimeoniDipartimento di InformaticaUniv. "Ca’ Foscari" di [email protected] propose an integrated approach to the functional andperformance analysis of Software Architectures (SAs) basedon Stochastic Process Algebras (SPAs) and Queueing Net-works (QNs), in order to combine their main advantages:formal techniques for the verification of functional proper-ties of systems for SPAs, and efficient performance analysisfor QNs. We first introduce Æmilia, a SPA based archi-tectural description language for the compositional, graph-ical and hierarchical modeling of SAs, which is equippedwith suitable checks for the detection of architectural mis-matches. Then we present a systematic approach to deriveQN models from Æmilia specifications. This is based on theidentification of three different classes of QN basic elements– arrival processes, buffers, and service processes – and onsyntactic restrictions to be imposed to Æmilia specifications,so that each architectural component directly falls into oneof the three classes. Although performance analysis couldbe carried out directly on the Markov chain (MC) under-lying an Æmilia specification, having a QN model allowsperformance indices to be evaluated possibly by exact prod-uct form solutions or by well known approximate methods.Furthermore, unlike the underlying MC, the high level ofabstraction of the QN model should ease the interpretationof the performance results at the architectural descriptionlevel.1. INTRODUCTIONSoftware Architecture (SA) is an emerging field withinsoftware engineering aiming at describing both the struc-ture and the behavior of software systems at a high levelof abstraction [18, 17]. The static and behavioral descrip-tions characterize, at an early stage of development, the ba-sic design choices on the system under consideration, whichclearly influence the subsequent development and deploy-ment phases. Appropriate languages and tools are then re-quired, in order to support SA with a suitable formalizationof the architecture descriptions and the automatic analysisof their functional properties.There is moreover a growing interest in quantitative anal-ysis of software systems, and it has been recognized in thelast years that performance analysis should be integratedin the software development life cycle since the early stages(see, e.g., [20, 21]). In particular, SAs have been devisedas the appropriate design level to conduct early predictiveperformance analysis, thus allowing for a choice among al-ternative architectures on the basis of quantitative aspects.In this paper we propose an integrated approach to thefunctional and performance analysis of SAs based on Stochas-tic Process Algebras (SPAs) and Queueing Networks (QNs).The idea is to combine the main advantages of the twoframeworks: formal techniques for system specification andverification of functional properties for SPAs, and efficientperformance analysis for QNs.SPA (see, e.g., [11, 10, 6]) is a well known formal spec-ification technique for concurrent and distributed systems.Its main features, i.e. composability – which allows systemdescriptions to be built in a modular and hierarchical way– and abstraction – which allows the internal details of asystem description to be hidden at analysis time – makeSPA suited to work with at the architectural level of de-sign. Compared to classical process algebra (see, e.g., [16]),besides the purely functional aspects with SPA it is possi-ble to express activity durations by using random variables.In addition to functional verification (e.g. via model check-ing [7]), this permits the quantitative analysis of the mod-eled system through the construction and solution of theunderlying stochastic process.QNs (see, e.g., [15, 14, 13]) have been widely applied assystem performance models. Classical QNs represent re-source sharing systems and can be solved by efficient algo-rithms, which do not require the construction of the under-lying stochastic process. Moreover, extensions of classicalQNs have been introduced in order to represent other inter-esting features of real systems, such as synchronization andconcurrency constraints, finite capacity queue and memoryconstraints, and simultaneous resource possession. Some ap-proximate solution techniques have been defined for severaltypes of extended QNs.The presentation of our integrated approach starts withthe introduction of Æmilia, an architectural description lan-guage (ADL) based on an expressive SPA called EMPAgr[6].Æmilia provides a formal framework for the compositional,graphical, and hierarchical modeling of software systems,which is equipped with some checks inspired by [3, 4] for thedetection of possible architectural mismatches. The timingPermission to make digital or hard copies of part or all of this work or personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. WOSP '02, July 24-26, 2002 Rome, Italy © 2002 ACM ISBN 1-1-58113-563-7 02/07 …$5.00 190of the durational actions is mainly expressed by exponentialrandom variables, so that the underlying stochastic processyields a Markov Chain (MC). Although performance anal-ysis could be carried on directly by Æmilia, this requiresthe construction and solution of the underlying MC, whosestate space explosion soon makes the analysis unfeasible.Moreover the MC is a flat model that does not reflect thestructure of the specified SA, thus hampering the interpreta-tion of the performance analysis results at the architecturaldescription level.In order to overcome these two drawbacks related to theefficient evaluation of performance indices and with the pos-sibility of getting some feedback at the architectural de-scription level in case of poor performance, we propose anapproach to derive QN models from Æmilia specifications.More precisely, we define a mapping from Æmilia to QNsbased on the identification of three different classes of