A formal approach to modeling and performance analysis of shared channels for real-time services in W-CDMA 3G systems