Charging is one of the most important functionalities in a telecommunication service system. In a general packet radio service (GPRS) wireless network, the load of charging information flow depends on the intensity of call traffic and the size of charging records. During busy hours, the GPRS network might not be able to transfer charging records on a timely basis if new charging records are generated too fast. On the other hand, when a call happens, the related charging information must be collected and transferred to the billing system. If a failure of the data link occurs, a secondary data link must be employed to transfer the charging information. However, this redundant operation might result in charging information duplication. This paper formally addresses these two issues. A timed Petri net model is built to support the analysis of the charging system performance versus various factors when the system works in the normal status, which, in particular, gives the maximum supportable busy hour call attempts of the GPRS network. The Petri net approach is also used to model and verify the correctness of the redundancy operation in case a connection failure occurs.