For a successful route request in Mobile Ad-hoc Networks (MANETs), it is important to know that routing protocols work cor-rectly. On the other hand,this phenomenon acts randomly and it is not often possible to predict their act from one moment to the next. One way for ensuring correct operation of the protocol is to develop a formalmodeland analyzeit. Stochastic Petri Net (SPN) is a formalmode-linglanguage which causes the analytical model to be a formal model. Also, prediction of future system's behavior is done in a shorter time than simulation. In this paper, an analytical model based on SPN was presented for TAODV routing protocol. The results showed thatthe analytical model acted like simulation model in terms of reliability,availability, andmean time tosecurity failure parameters.