Abstract:We present a method for automatic modeling in SMV of a parameterized system based on its corresponding Murphi Model. Modeling in Murphi for parameterized systems is easy because its parameterization feature, and a Murphi model code is relatively small and is not very complex to read, understand and modify. On the other hand, an SMV model could give more powerful operations, such as quick invariant checking and bounded model checking, but it is very hard to model in SMV for a parameterized system and to maintain an SMV model. We present a semantic model which is well able to describe a parameterized system, then analyze a Murphi model to create its semantic model, finally we get its corresponding SMV model which is effective for research work automatically by a series of conversion strategies.