Besides traditional verification of system functions, performance evaluation in modern hardware and software systems has received extensive attention. Performance evaluation aims at obtaining quantitative measures of the system to test whether reliability-related properties are warranted. In this paper, model of the system is expressed in the form of IMC, a mixed model for describing both action-based and state-based systems. And by converting performance properties of the system into aCSL formulae, we can formally verify them by model checking. To accelerate the process of IMC performance evaluation, a modified version of ant colony algorithm is proposed in the paper. Compared with other numerical methods, the ant colony algorithm reduces unnecessary model elements and the execution efficiency is largely improved to tackle more complex system performance evaluation problems.