In this paper we present a formal approach to analyse performance for distributed systems, which is integrated in the early stages of the software development process. We propose to model the software system in a pragmatic way using as a design technique the well-known design patterns; from these models, the corresponding formal performance model, in terms of Petri nets, is obtained semiautomatically by applying a set of translation rules. Finally, the formal performance model is analysed, using analytical techniques, in order to study the performance of the system. Moreover, another benefit of the proposal is that it is possible to predict the behaviour of the system without the necessity of implementing it. To illustrate the proposal, we apply it to a software retrieval service system designed using mobile agents.