Software architecture has become an increasingly important research topic in recent years. Concurrently much more attention has been paid to methods of evaluating non functional attributes of these architectures. However, in current architectural description languages (ADLs) based on a formal and abstract model of system behavior, there is a notable lack of support for representing and reasoning about non functional attributes. In this paper, we propose ACME+ ADL as an extension of ACME ADL and discuss our quantitative model for formal analysis of software architectures. This paper gives an overview of our formal approach for describing software architectures and analyzing their performance, reliability, maintainability and availability. The proposed model is supported by an automated tool that transforms an architecture described in ACME+ into a set of inequalities characterizing system non functional attributes. These inequalities are then solved using Mathematica in order to obtain system properties as function of its components and connectors properties.