Abstract: The architecture we previously constructed for autonomous underwater vehicles (AUV) only remains in the system block level. To cope with this insufficiency, the architecture is modeled and its correctness is theoretically analyzed in this paper. Firstly, our previous work, that is, a generalized architecture for AUVs, is presented. Then, according to its characteristics of modular packaging and hierarchical organization, the object-oriented Petri net is adopted to model this architecture. Based upon this, the mission reachability problem is focused and a sufficient criteria is proposed. Thus, the correctness of the timing and logic of this architecture is thoroughly demonstrated. Finally, semi-physical experiments are carried out to validate the architecture.