TY - JFULL AU - Zhang Xiuping and Yang Guowu and Zheng Desheng PY - 2011/9/ TI - MMU Simulation in Hardware Simulator Based-on State Transition Models T2 - International Journal of Computer and Information Engineering SP - 967 EP - 972 VL - 5 SN - 1307-6892 UR - https://publications.waset.org/pdf/10961 PU - World Academy of Science, Engineering and Technology NX - Open Science Index 56, 2011 N2 - Embedded hardware simulator is a valuable computeraided tool for embedded application development. This paper focuses on the ARM926EJ-S MMU, builds state transition models and formally verifies critical properties for the models. The state transition models include loading instruction model, reading data model, and writing data model. The properties of the models are described by CTL specification language, and they are verified in VIS. The results obtained in VIS demonstrate that the critical properties of MMU are satisfied in the state transition models. The correct models can be used to implement the MMU component in our simulator. In the end of this paper, the experimental results show that the MMU can successfully accomplish memory access requests from CPU. ER -