Public/private decision makers have faced challenges to improve healthcare services for supporting the increasing demand and simultaneously reducing the associated costs. Although the adoption of information and communication technologies (ICTs) are important in this context, the current service status should be firstly examined and different configurations/scenarios quantitatively evaluated before any further adjustment. Formal methods are of great importance, since they provide mathematical means for quantitative evaluation of systems and allow property analysis/verification. This paper presents an approach based on stochastic Petri nets for the performance evaluation of medical imaging service, adopting a real-world case study to demonstrate the feasibility of the proposed approach.