Service-based applications (SBAs) are a new category of software, built according to the principle of service-orientation. SBAs may compose third-parties, independent services to build new, added-value service compositions. The distributed ownership and the evolving nature of SBAs make the quality assurance process very important. This is especially true for non-functional requirements, because the quality of service (QoS) provided by a composite service depends on the QoS of the external services in the composition. In terms of quality assurance for SBAs, it is crucial to study both how to formally specify the interactions of SBAs and also how to perform their automatic verification. In this thesis we focus on the verification of the quantitative properties of SBAs captured by some specification patterns specific to the provisioning of SBAs. Specifications are written using the SOLOIST specification language and the verification is performed using the Zot model checker. The thesis describes two ways of translating SOLOIST specifications into a form that can be processed by Zot. As part of this thesis we built a tool that is able to perform bounded history checking on execution traces of SBAs interactions, against properties specified in SOLOIST. We also include results of the experimental evaluation conducted to assess the efficiency of the proposed translations.